src/Pure/Tools/build_cluster.scala
changeset 78582 63f06b935a1f
parent 78581 1384593459b4
child 78584 92ef737f412c
--- a/src/Pure/Tools/build_cluster.scala	Sat Aug 26 13:47:03 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Sat Aug 26 13:48:14 2023 +0200
@@ -302,8 +302,8 @@
 
     _workers =
       for (session <- _sessions) yield {
-        Future.thread(session.host.message("run")) {
-          Exn.release(capture(session.host, "run") { session.start() })
+        Future.thread(session.host.message("work")) {
+          Exn.release(capture(session.host, "work") { session.start() })
         }
       }
   }