author | wenzelm |
Sat, 26 Aug 2023 13:48:14 +0200 | |
changeset 78582 | 63f06b935a1f |
parent 78581 | 1384593459b4 |
child 78583 | 8f11794211ef |
--- 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() }) } } }