# HG changeset patch
# User wenzelm
# Date 1692987053 -7200
# Node ID 2dad5335cc57053856d0d5125a6f3c1a8129cb53
# Parent  5ccf921a2c3deb574e4042a2c03915ebb5b0fc35
tuned message: failure can happen towards the end, e.g. due to failed sessions or progress.stopped;

diff -r 5ccf921a2c3d -r 2dad5335cc57 src/Pure/Tools/build_cluster.scala
--- 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() })
         }
       }
   }