changeset 73523 | 2cd23d587db9 |
parent 73521 | a6ca869af096 |
--- a/lib/Tools/version Wed Mar 31 22:10:56 2021 +0200 +++ b/lib/Tools/version Wed Mar 31 22:58:17 2021 +0200 @@ -62,7 +62,7 @@ ## main if [ -z "$SHORT_ID" -a -z "$TAGS" ]; then - echo 'repository version' # filled in automatically! + echo "$ISABELLE_NAME" fi HG_ARCHIVAL="$ISABELLE_HOME/.hg_archival.txt"