tuned;
authorwenzelm
Sat, 27 Mar 2021 18:03:50 +0100
changeset 73737 9830d7981ad0
parent 73736 92db3e31fae3
child 73738 804e75127f29
tuned;
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