Admin/makedist
changeset 37341 b0eda879d735
parent 37217 b2769ba027b0
child 37459 4f79bb1aaf50
     1.1 --- a/Admin/makedist	Sun Jun 06 17:37:44 2010 +0200
     1.2 +++ b/Admin/makedist	Sun Jun 06 18:04:59 2010 +0200
     1.3 @@ -172,10 +172,10 @@
     1.4  perl -pi -e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README
     1.5  
     1.6  
     1.7 -# create archives
     1.8 +# create archive
     1.9  
    1.10  echo "###"
    1.11 -echo "### Creating archives ..."
    1.12 +echo "### Creating archive ..."
    1.13  echo "###"
    1.14  
    1.15  cd "$DISTBASE"
    1.16 @@ -210,3 +210,5 @@
    1.17  
    1.18  rm -rf "${DISTNAME}-old"
    1.19  
    1.20 +
    1.21 +echo "DONE"