From b04b5c0ad3108ab13eb26739e57144341d0b2d38 Mon Sep 17 00:00:00 2001
From: Max Horn <max@quendi.de>
Date: Mon, 9 Oct 2023 14:33:45 +0200
Subject: [PATCH] improve

---
 dev/make_dist.sh | 39 ++++++++++++++++++++++++---------------
 1 file changed, 24 insertions(+), 15 deletions(-)

diff --git a/dev/make_dist.sh b/dev/make_dist.sh
index 8f60ad9ca4..00664be6bf 100755
--- a/dev/make_dist.sh
+++ b/dev/make_dist.sh
@@ -8,19 +8,28 @@ FLINT_PATCH=$3
 git_ref=${4-origin/flint-$FLINT_MAJOR.$FLINT_MINOR}
 
 archive_prefix="flint-$FLINT_MAJOR.$FLINT_MINOR.$FLINT_PATCH"
+tmpdir=/tmp/flint_release
 
-git archive --format tar --prefix "${archive_prefix}/" ${git_ref} > ../${archive_prefix}.tar; gzip ../${archive_prefix}.tar
-git archive --format zip --prefix "${archive_prefix}/" ${git_ref} > ../${archive_prefix}.zip
-
-# TODO:
-# - remove stuff:
-# .build_dependencies
-# .check_post_install
-# .gitattributes
-# .github
-# .gitignore
-# .travis.yml
-# dev/
-#
-# - ensure various generated files are included :
-#   config/
+mkdir -p ${tmpdir}
+git archive --format tar.gz --prefix "${archive_prefix}/" ${git_ref} > ${tmpdir}/${archive_prefix}.tar.gz
+
+pushd ${tmpdir}
+tar -xvf ${archive_prefix}.tar.gz
+popd
+
+# copy some files that should be included in the distribution archive
+cp -r config ${tmpdir}/${archive_prefix}/
+cp configure ${tmpdir}/${archive_prefix}/
+cp src/config.h.in ${tmpdir}/${archive_prefix}/src/
+
+# go to the source directory for further adjustments
+cd ${tmpdir}/${archive_prefix}
+
+# remove some things we don't want to install
+rm -rf .[a-z]*  # no dot files
+rm -rf dev
+
+# now leave and re-create the source archive
+cd ..
+rm ${archive_prefix}.tar.gz
+tar -cvzf ${archive_prefix}.tar.gz ${archive_prefix}