src/Pure/Build/build_cluster.scala
changeset 82711 5bd0d6a8fd7a
parent 80200 5f053991315c
child 82718 e1a8753eaad7
--- 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)