| 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() }) } } }