# HG changeset patch
# User wenzelm
# Date 1625054594 -7200
# Node ID 9849943b83fa14c6fb1a4128ccd721fcd5fc942e
# Parent  4df63c3a4c4f532575bed3e52b4e23965a64f36f
tuned;

diff -r 4df63c3a4c4f -r 9849943b83fa src/Pure/System/isabelle_env.scala
--- a/src/Pure/System/isabelle_env.scala	Wed Jun 30 13:49:32 2021 +0200
+++ b/src/Pure/System/isabelle_env.scala	Wed Jun 30 14:03:14 2021 +0200
@@ -21,16 +21,19 @@
   /** bootstrap information **/
 
   def bootstrap_directory(
-    preference: String, envar: String, property: String, description: String): String =
+    preference: String, variable: String, property: String, description: String): String =
   {
-    val value =
-      proper_string(preference) orElse  // explicit argument
-      proper_string(System.getenv(envar)) orElse  // e.g. inherited from running isabelle tool
-      proper_string(System.getProperty(property)) getOrElse  // e.g. via JVM application boot process
-      error("Unknown " + description + " directory")
+    val a = preference  // explicit argument
+    val b = System.getenv(variable)  // e.g. inherited from running isabelle tool
+    val c = System.getProperty(property)  // e.g. via JVM application boot process
+    val dir =
+      if (a != null && a.nonEmpty) a
+      else if (b != null && b.nonEmpty) b
+      else if (c != null && c.nonEmpty) c
+      else error("Unknown " + description + " directory")
 
-    if ((new JFile(value)).isDirectory) value
-    else error("Bad " + description + " directory " + quote(value))
+    if ((new JFile(dir)).isDirectory) dir
+    else error("Bad " + description + " directory " + quote(dir))
   }