tuned message: failure can happen towards the end, e.g. due to failed sessions or progress.stopped;
--- a/src/Pure/Tools/build_cluster.scala Fri Aug 25 20:08:32 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala Fri Aug 25 20:10:53 2023 +0200
@@ -292,8 +292,8 @@
_workers =
for (session <- _sessions) yield {
- Future.thread(session.host.message("start")) {
- Exn.release(capture(session.host, "start") { session.start() })
+ Future.thread(session.host.message("run")) {
+ Exn.release(capture(session.host, "run") { session.start() })
}
}
}