--- a/lib/Tools/version Thu Mar 15 11:27:32 2018 +0100
+++ b/lib/Tools/version Thu Mar 15 11:44:07 2018 +0100
@@ -60,7 +60,7 @@
if [ -n "$ISABELLE_ID" ]; then
echo "$ISABELLE_ID"
else
- "${HG:-hg}" id --repository "$ISABELLE_HOME" --id 2>/dev/null || echo undefined
+ "${HG:-hg}" -R "$ISABELLE_HOME" id -i -r tip 2>/dev/null || echo undefined
fi
else
echo 'unidentified repository version' # filled in automatically!
--- a/src/Pure/General/http.scala Thu Mar 15 11:27:32 2018 +0100
+++ b/src/Pure/General/http.scala Thu Mar 15 11:44:07 2018 +0100
@@ -141,11 +141,7 @@
val welcome: Handler =
get("/", arg =>
if (arg.uri.toString == "/") {
- val id =
- Isabelle_System.getenv("ISABELLE_ID") match {
- case "" => Mercurial.repository(Path.explode("~~")).id()
- case id => id
- }
+ val id = Isabelle_System.isabelle_id()
Some(Response.text("Welcome to Isabelle/" + id + ": " + Distribution.version))
}
else None)
--- a/src/Pure/System/isabelle_system.scala Thu Mar 15 11:27:32 2018 +0100
+++ b/src/Pure/System/isabelle_system.scala Thu Mar 15 11:44:07 2018 +0100
@@ -144,6 +144,10 @@
def cygwin_root(): String = getenv_strict("CYGWIN_ROOT")
+ def isabelle_id(): String =
+ proper_string(getenv("ISABELLE_ID")) getOrElse
+ Mercurial.repository(Path.explode("~~")).id()
+
/** file-system operations **/