diff -r 4cba4e250c28 -r a6ca869af096 lib/Tools/version
--- a/lib/Tools/version	Wed Mar 31 18:12:46 2021 +0200
+++ b/lib/Tools/version	Wed Mar 31 21:44:29 2021 +0200
@@ -72,24 +72,38 @@
 
 if [ -n "$SHORT_ID" ]; then
   if [ -f "$ISABELLE_HOME/etc/ISABELLE_ID" ]; then
-    ID="$(cat "$ISABELLE_HOME/etc/ISABELLE_ID")"
-    echo "$ID"
+    RESULT="$(cat "$ISABELLE_HOME/etc/ISABELLE_ID")"
+    RC="$?"
+  elif [ -d "$ISABELLE_HOME/.hg" ]; then
+    RESULT=$("${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null)
+    RC="$?"
   elif [ -f "$HG_ARCHIVAL" ]; then
     RESULT="$(grep "^node:" < "$HG_ARCHIVAL" | cut -d " " -f2 | head -c12)"
-    [ -n "$RESULT" ] && echo "$RESULT"
-  elif [ -d "$ISABELLE_HOME/.hg" ]; then
-    "${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null || exit "$?"
+    RC="$?"
+  else
+    RESULT=""
+    RC="0"
+  fi
+  if [ "$RC" -ne 0 ]; then
+    exit "$RC"
+  elif [ -n "$RESULT" ]; then
+    echo "$RESULT"
   fi
 fi
 
 if [ -n "$TAGS" ]; then
-  RESULT=""
-  if [ -d "$ISABELLE_HOME/.hg" ]; then
+  if [ -f "$ISABELLE_HOME/etc/ISABELLE_TAGS" ]; then
+    RESULT="$(cat "$ISABELLE_HOME/etc/ISABELLE_TAGS")"
+    RC="$?"
+  elif [ -d "$ISABELLE_HOME/.hg" ]; then
     RESULT=$("${HG:-hg}" -R "$ISABELLE_HOME" id -t 2>/dev/null)
     RC="$?"
   elif [ -f "$HG_ARCHIVAL" ]; then
     RESULT="$(grep "^tag:" < "$HG_ARCHIVAL" | cut -d " " -f2)"
     RC="$?"
+  else
+    RESULT=""
+    RC="0"
   fi
   if [ "$RC" -ne 0 ]; then
     exit "$RC"