tuned signature;

--- a/src/Pure/Admin/build_history.scala	Sat Oct 20 15:36:32 2018 +0200
+++ b/src/Pure/Admin/build_history.scala	Sun Oct 21 14:25:51 2018 +0200
@@ -35,12 +35,12 @@
     {
       val windows_32 = "x86-windows"
       val windows_64 = "x86_64-windows"
-      val platform_32 = other_isabelle("getenv -b ISABELLE_PLATFORM32").check.out
-      val platform_64 = other_isabelle("getenv -b ISABELLE_PLATFORM64").check.out
-      val platform_family = other_isabelle("getenv -b ISABELLE_PLATFORM_FAMILY").check.out
+      val platform_32 = other_isabelle.getenv("ISABELLE_PLATFORM32")
+      val platform_64 = other_isabelle.getenv("ISABELLE_PLATFORM64")
+      val platform_family = other_isabelle.getenv("ISABELLE_PLATFORM_FAMILY")
 
       val polyml_home =
-        try { Path.explode(other_isabelle("getenv -b ML_HOME").check.out).dir }
+        try { Path.explode(other_isabelle.getenv("ML_HOME")).dir }
         catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) }
 
       def ml_home(platform: String): Path = polyml_home + Path.explode(platform)
@@ -192,7 +192,7 @@
 
       val isabelle_output =
         other_isabelle.isabelle_home_user + Path.explode("heaps") +
-          Path.explode(other_isabelle("getenv -b ML_IDENTIFIER").check.out)
+          Path.explode(other_isabelle.getenv("ML_IDENTIFIER"))
       val isabelle_output_log = isabelle_output + Path.explode("log")
       val isabelle_base_log = isabelle_output + Path.explode("../base_log")
 

--- a/src/Pure/Admin/other_isabelle.scala	Sat Oct 20 15:36:32 2018 +0200
+++ b/src/Pure/Admin/other_isabelle.scala	Sun Oct 21 14:25:51 2018 +0200
@@ -52,8 +52,10 @@
   def resolve_components(echo: Boolean): Unit =
     other_isabelle("components -a", redirect = true, echo = echo).check
 
-  val isabelle_home_user: Path =
-    Path.explode(other_isabelle("getenv -b ISABELLE_HOME_USER").check.out)
+  def getenv(name: String): String =
+    other_isabelle("getenv -b " + Bash.string(name)).check.out
+
+  val isabelle_home_user: Path = Path.explode(getenv("ISABELLE_HOME_USER"))
 
   val etc: Path = isabelle_home_user + Path.explode("etc")
   val etc_settings: Path = etc + Path.explode("settings")