improve

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}