src/Pure/Build/build_cluster.scala
changeset 82723 740cf003658b
parent 82718 e1a8753eaad7
--- 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)