# HG changeset patch
# User wenzelm
# Date 1477486228 -7200
# Node ID d75397e0aad5577f2b3c83e0fd55642f578fadb4
# Parent  7fa053298f67b8c1b948998eb772ca59c5f494b3
tuned;

diff -r 7fa053298f67 -r d75397e0aad5 Admin/lib/Tools/makedist
--- a/Admin/lib/Tools/makedist	Wed Oct 26 12:22:58 2016 +0100
+++ b/Admin/lib/Tools/makedist	Wed Oct 26 14:50:28 2016 +0200
@@ -123,7 +123,7 @@
 
 # retrieve repository archive
 
-echo "### Retrieving Mercurial repository $VERSION"
+echo "### Retrieving Mercurial repository version $VERSION"
 
 "$HG" --repository "$ISABELLE_HOME" archive --type files -r "$IDENT" "$DIR" || \
   fail "Failed to retrieve $VERSION"