# HG changeset patch
# User wenzelm
# Date 1275840299 -7200
# Node ID b0eda879d735625f0bfdda07f763c7b40ecbdd35
# Parent  5350cd2ae2c4701135cbc10bec64e552c98c1c93
tuned;

diff -r 5350cd2ae2c4 -r b0eda879d735 Admin/makedist
--- 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"