# HG changeset patch
# User wenzelm
# Date 1616926897 -7200
# Node ID 5d750df8e89402c47faa3a268bc7864e990f0446
# Parent  001097314d0926dfea5e26d173e1a5f31584ec7c
more robust;

diff -r 001097314d09 -r 5d750df8e894 lib/Tools/version
--- a/lib/Tools/version	Sun Mar 28 12:10:14 2021 +0200
+++ b/lib/Tools/version	Sun Mar 28 12:21:37 2021 +0200
@@ -74,7 +74,7 @@
   if [ -d "$ISABELLE_HOME/.hg" ]; then
     "${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null || exit "$?"
   elif [ -f "$HG_ARCHIVAL" ]; then
-    RESULT="$(fgrep node: < "$HG_ARCHIVAL" | cut -d " " -f2 | head -c12)"
+    RESULT="$(grep "^node:" < "$HG_ARCHIVAL" | cut -d " " -f2 | head -c12)"
     [ -n "$RESULT" ] && echo "$RESULT"
   elif [ -n "$ISABELLE_ID" ]; then
     echo "$ISABELLE_ID"
@@ -87,7 +87,7 @@
     RESULT=$("${HG:-hg}" -R "$ISABELLE_HOME" id -t 2>/dev/null)
     RC="$?"
   elif [ -f "$HG_ARCHIVAL" ]; then
-    RESULT="$(fgrep tag: < "$HG_ARCHIVAL" | cut -d " " -f2)"
+    RESULT="$(grep "^tag:" < "$HG_ARCHIVAL" | cut -d " " -f2)"
     RC="$?"
   fi
   if [ "$RC" -ne 0 ]; then