proper settings for hostname: allow to adjust it in user space;
authorwenzelm
Sun, 26 Feb 2023 13:06:19 +0100
changeset 77373 eaf234b0c849
parent 77372 44fe9fe96130
child 77374 268bf61631ec
proper settings for hostname: allow to adjust it in user space;
lib/scripts/getsettings
src/Pure/System/isabelle_system.scala
--- a/lib/scripts/getsettings	Sun Feb 26 11:55:24 2023 +0100
+++ b/lib/scripts/getsettings	Sun Feb 26 13:06:19 2023 +0100
@@ -78,6 +78,8 @@
 
 ISABELLE_NAME="${ISABELLE_IDENTIFIER:-Isabelle}"
 
+ISABELLE_HOSTNAME="$(hostname -s)"
+
 
 # components
 
--- a/src/Pure/System/isabelle_system.scala	Sun Feb 26 11:55:24 2023 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sun Feb 26 13:06:19 2023 +0100
@@ -47,6 +47,8 @@
     proper_string(getenv(name, env)) getOrElse
       error("Undefined Isabelle environment variable: " + quote(name))
 
+  def hostname(): String = getenv_strict("ISABELLE_HOSTNAME")
+
 
   /* services */
 
@@ -499,8 +501,6 @@
     }
   }
 
-  def hostname(): String = bash("hostname -s").check.out
-
   def open(arg: String): Unit =
     bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &")