WIP5

dev/make_dist.sh

@@ -7,13 +7,17 @@ git_ref=${4:-HEAD}
 archive_prefix="flint-$flint_version"
 tmpdir=$PWD/..
 
+echo "Exporting from git"
 mkdir -p ${tmpdir}
 git archive --format tar.gz --prefix "${archive_prefix}/" ${git_ref} > ${tmpdir}/${archive_prefix}.tar.gz
 
+echo "Extracting"
 pushd ${tmpdir}
-tar -xvf ${archive_prefix}.tar.gz
+tar -xf ${archive_prefix}.tar.gz
+rm ${archive_prefix}.tar.gz
 popd
 
+echo "Adding and removing files"
 # copy some files that should be included in the distribution archive
 cp -r config ${tmpdir}/${archive_prefix}/
 cp configure ${tmpdir}/${archive_prefix}/
@@ -27,6 +31,6 @@ rm -rf .[a-z]*  # no dot files
 rm -rf dev
 
 # now leave and re-create the source archive
-cd ..
-rm ${archive_prefix}.tar.gz
+cd ${tmpdir}
+echo "Create new tarball"
 tar -cvzf ${archive_prefix}.tar.gz ${archive_prefix}