diff -r d1a944a15def -r 740cf003658b src/Pure/Build/build_cluster.scala --- a/src/Pure/Build/build_cluster.scala Sun Jun 15 23:03:12 2025 +0200 +++ b/src/Pure/Build/build_cluster.scala Sun Jun 15 23:09:43 2025 +0200 @@ -210,8 +210,8 @@ def start(): Process_Result = { 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) + error("Bad ML_PLATFORM: found " + quote(build_cluster_ml_platform) + + ", but expected " + quote(build_context.ml_platform)) } val build_options = for { option <- options.iterator if option.for_build_sync } yield options.spec(option.name)