--- 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