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