diff -r 6e20976d58f5 -r 0e880b793db1 lib/Tools/version
--- a/lib/Tools/version	Sat Mar 27 17:05:36 2021 +0100
+++ b/lib/Tools/version	Sat Mar 27 17:13:15 2021 +0100
@@ -59,8 +59,12 @@
 if [ -n "$SHORT_ID" ]; then
   if [ -n "$ISABELLE_ID" ]; then
     echo "$ISABELLE_ID"
+  elif [ -d "$ISABELLE_HOME/.hg" ]; then
+    "${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null || echo undefined
+  elif [ -f "$ISABELLE_HOME/.hg_archival.txt" ]; then
+    fgrep node: < "$ISABELLE_HOME/.hg_archival.txt" | cut -d " " -f2 | head -c12
   else
-    "${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null || echo undefined
+    echo undefined
   fi
 else
   echo 'repository version'    # filled in automatically!