diff -r 8d42bf3b821d -r e1a8753eaad7 src/Pure/Build/build_cluster.scala --- a/src/Pure/Build/build_cluster.scala Sun Jun 15 13:40:03 2025 +0200 +++ b/src/Pure/Build/build_cluster.scala Sun Jun 15 15:19:03 2025 +0200 @@ -208,7 +208,7 @@ } def start(): Process_Result = { - val build_cluster_ml_platform = build_cluster_isabelle.ml_platform + val build_cluster_ml_platform = build_cluster_isabelle.ml_settings.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)