# HG changeset patch
# User wenzelm
# Date 1677413179 -3600
# Node ID eaf234b0c849c9fd09acc2724625169e166a159e
# Parent  44fe9fe96130dbb5b6102ad564cd697a185a9fee
proper settings for hostname: allow to adjust it in user space;

diff -r 44fe9fe96130 -r eaf234b0c849 lib/scripts/getsettings
--- 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
 
diff -r 44fe9fe96130 -r eaf234b0c849 src/Pure/System/isabelle_system.scala
--- 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 &")