# HG changeset patch
# User wenzelm
# Date 1749928777 -7200
# Node ID 5bd0d6a8fd7a390796f9f56e0cd33b96e4952ff7
# Parent  e09e986731e9dd419548a599e86a665ba20f9f86
clarified signature;

diff -r e09e986731e9 -r 5bd0d6a8fd7a src/Pure/Build/build_cluster.scala
--- a/src/Pure/Build/build_cluster.scala	Sat Jun 14 21:07:09 2025 +0200
+++ b/src/Pure/Build/build_cluster.scala	Sat Jun 14 21:19:37 2025 +0200
@@ -208,7 +208,7 @@
     }
 
     def start(): Process_Result = {
-      val build_cluster_ml_platform = build_cluster_isabelle.getenv("ML_PLATFORM")
+      val build_cluster_ml_platform = build_cluster_isabelle.ml_platform
       if (build_cluster_ml_platform != build_context.ml_platform) {
         error("Bad ML_PLATFORM: found " + build_cluster_ml_platform +
           ", but expected " + build_context.ml_platform)
diff -r e09e986731e9 -r 5bd0d6a8fd7a src/Pure/System/other_isabelle.scala
--- a/src/Pure/System/other_isabelle.scala	Sat Jun 14 21:07:09 2025 +0200
+++ b/src/Pure/System/other_isabelle.scala	Sat Jun 14 21:19:37 2025 +0200
@@ -68,12 +68,19 @@
     ssh.execute(bash_context("bin/isabelle getenv -b " + Bash.string(name)),
       settings = false).check.out
 
+  def getenv_strict(name: String): String =
+    proper_string(getenv(name)) getOrElse
+      error("Undefined Isabelle environment variable: " + quote(name) +
+        "\nISABELLE_HOME=" + isabelle_home)
+
   val settings: Isabelle_System.Settings = (name: String) => getenv(name)
 
   def expand_path(path: Path): Path = path.expand_env(settings)
   def bash_path(path: Path): String = Bash.string(expand_path(path).implode)
 
-  def ml_identifier: String = ML_Process.ml_identifier(env = settings)
+  def ml_system: String = getenv_strict("ML_SYSTEM")
+  def ml_platform: String = getenv_strict("ML_PLATFORM")
+  def ml_identifier: String = ml_system + "_" + ml_platform
 
   val isabelle_home_user: Path = expand_path(Path.explode("$ISABELLE_HOME_USER"))