more robust;
authorwenzelm
Sun, 28 Mar 2021 12:21:37 +0200
changeset 73764 5d750df8e894
parent 73763 001097314d09
child 73765 c526eb2c7ca0
more robust;
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