tuned;
authorwenzelm
Sun, 06 Jun 2010 18:04:59 +0200
changeset 37341b0eda879d735
parent 37339 5350cd2ae2c4
child 37342 7299d0bf82c5
tuned;
Admin/makedist
     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"