# HG changeset patch
# User wenzelm
# Date 1616864630 -3600
# Node ID 9830d7981ad0b1e8fd32268fa40002869bc03955
# Parent  92db3e31fae3e3ffcbc3fed58e19d67feb2642b3
tuned;

diff -r 92db3e31fae3 -r 9830d7981ad0 lib/Tools/version
--- a/lib/Tools/version	Sat Mar 27 18:01:41 2021 +0100
+++ b/lib/Tools/version	Sat Mar 27 18:03:50 2021 +0100
@@ -65,11 +65,13 @@
   echo 'repository version'    # filled in automatically!
 fi
 
+HG_ARCHIVAL="$ISABELLE_HOME/.hg_archival.txt"
+
 if [ -n "$SHORT_ID" ]; then
   if [ -d "$ISABELLE_HOME/.hg" ]; then
     "${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null || exit "$?"
-  elif [ -f "$ISABELLE_HOME/.hg_archival.txt" ]; then
-    RESULT="$(fgrep node: < "$ISABELLE_HOME/.hg_archival.txt" | cut -d " " -f2 | head -c12)"
+  elif [ -f "$HG_ARCHIVAL" ]; then
+    RESULT="$(fgrep node: < "$HG_ARCHIVAL" | cut -d " " -f2 | head -c12)"
     [ -n "$RESULT" ] && echo "$RESULT"
   elif [ -n "$ISABELLE_ID" ]; then
     echo "$ISABELLE_ID"
@@ -81,8 +83,8 @@
   if [ -d "$ISABELLE_HOME/.hg" ]; then
     RESULT=$("${HG:-hg}" -R "$ISABELLE_HOME" id -t 2>/dev/null)
     RC="$?"
-  elif [ -f "$ISABELLE_HOME/.hg_archival.txt" ]; then
-    RESULT="$(fgrep tag: < "$ISABELLE_HOME/.hg_archival.txt" | cut -d " " -f2)"
+  elif [ -f "$HG_ARCHIVAL" ]; then
+    RESULT="$(fgrep tag: < "$HG_ARCHIVAL" | cut -d " " -f2)"
     RC="$?"
   fi
   if [ "$RC" -ne 0 ]; then