changeset 37341 | b0eda879d735 |
parent 37217 | b2769ba027b0 |
child 37356 | 4f79bb1aaf50 |
--- a/Admin/makedist Sun Jun 06 17:37:44 2010 +0200 +++ b/Admin/makedist Sun Jun 06 18:04:59 2010 +0200 @@ -172,10 +172,10 @@ perl -pi -e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README -# create archives +# create archive echo "###" -echo "### Creating archives ..." +echo "### Creating archive ..." echo "###" cd "$DISTBASE" @@ -210,3 +210,5 @@ rm -rf "${DISTNAME}-old" + +echo "DONE"