lib/Tools/version
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"