tuned messages (again);
authorwenzelm
Sat, 26 Aug 2023 13:48:14 +0200
changeset 78582 63f06b935a1f
parent 78581 1384593459b4
child 78583 8f11794211ef
tuned messages (again);
src/Pure/Tools/build_cluster.scala
--- 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() })
         }
       }
   }