more accurate isabelle_id: parent directory is not necessarily at tip;
authorwenzelm
Thu, 15 Mar 2018 22:28:20 +0100
changeset 67872 39b27d38a54c
parent 67871 195ff117894c
child 67873 e4e740ba74a4
more accurate isabelle_id: parent directory is not necessarily at tip;
lib/Tools/version
src/Pure/System/isabelle_system.scala
--- a/lib/Tools/version	Thu Mar 15 22:17:56 2018 +0100
+++ b/lib/Tools/version	Thu Mar 15 22:28:20 2018 +0100
@@ -60,7 +60,7 @@
   if [ -n "$ISABELLE_ID" ]; then
     echo "$ISABELLE_ID"
   else
-    "${HG:-hg}" -R "$ISABELLE_HOME" id -i -r tip 2>/dev/null || echo undefined
+    "${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null || echo undefined
   fi
 else
   echo 'repository version'    # filled in automatically!
--- a/src/Pure/System/isabelle_system.scala	Thu Mar 15 22:17:56 2018 +0100
+++ b/src/Pure/System/isabelle_system.scala	Thu Mar 15 22:28:20 2018 +0100
@@ -146,7 +146,7 @@
 
   def isabelle_id(): String =
     proper_string(getenv("ISABELLE_ID")) getOrElse
-      Mercurial.repository(Path.explode("~~")).id()
+      Mercurial.repository(Path.explode("~~")).parent()