tuned;
authorwenzelm
Wed, 26 Oct 2016 14:50:28 +0200
changeset 64404 d75397e0aad5
parent 64403 7fa053298f67
child 64405 81bac77929d9
tuned;
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"