# HG changeset patch
# User wenzelm
# Date 1275842093 -7200
# Node ID 7299d0bf82c594a61bac39c6ae2fadff13b92b14
# Parent  f3492868bbfdbbef5d69ba284f91d68848c9578e# Parent  b0eda879d735625f0bfdda07f763c7b40ecbdd35
merged

diff -r f3492868bbfd -r 7299d0bf82c5 Admin/makedist
--- a/Admin/makedist	Sun Jun 06 18:29:10 2010 +0200
+++ b/Admin/makedist	Sun Jun 06 18:34:53 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"