# HG changeset patch
# User wenzelm
# Date 1692793421 -7200
# Node ID 11cf77478d3ed11e6aea16355b4765382ffbfae2
# Parent  ed07f0ebf31cc810a44c674c9a74ae43a376adb7
more explicit check;

diff -r ed07f0ebf31c -r 11cf77478d3e src/Pure/Tools/build_cluster.scala
--- a/src/Pure/Tools/build_cluster.scala	Wed Aug 23 11:44:08 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Wed Aug 23 14:23:41 2023 +0200
@@ -148,6 +148,11 @@
     def init(): Unit = remote_isabelle.init()
 
     def start(): Process_Result = {
+      val remote_ml_platform = remote_isabelle.getenv("ML_PLATFORM")
+      if (remote_ml_platform != build_context.ml_platform) {
+        error("Bad ML_PLATFORM: found " + remote_ml_platform +
+          ", but expected " + build_context.ml_platform)
+      }
       val script =
         Build.build_worker_command(host,
           ssh = ssh,