From fc18da70438104f4dc1ddfa1d39984fdd3460a73 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?St=C3=A9phane=20Lesimple?= <speed47_github@speed47.net>
Date: Tue, 12 Jan 2021 21:14:56 +0100
Subject: [PATCH] chore: add CHANGELOG, TODO, CREDITS to dist

---
 .github/workflows/make-dist.sh | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/make-dist.sh b/.github/workflows/make-dist.sh
index e5a8851..fcbc3ea 100755
--- a/.github/workflows/make-dist.sh
+++ b/.github/workflows/make-dist.sh
@@ -42,7 +42,8 @@ if [ "$os" != "linux64" ]; then
   find dist -type f -name "*.a" -delete
 fi
 man -t documentation/dvdisaster.en.1 | ps2pdf - dist/dvdisaster.pdf
-cp dvdisaster documentation/dvdisaster.*.1 documentation/user-manual/manual.pdf dist/
+cp CHANGELOG TODO dvdisaster documentation/dvdisaster.*.1 documentation/user-manual/manual.pdf dist/
+cp CREDITS.en dist/CREDITS
 if command -v zip >/dev/null; then
     mv dist ${archive/.zip/}
     zip -9r $archive ${archive/.zip/}