tuned message: failure can happen towards the end, e.g. due to failed sessions or progress.stopped;
authorwenzelm
Fri, 25 Aug 2023 20:10:53 +0200
changeset 78579 2dad5335cc57
parent 78578 5ccf921a2c3d
child 78580 c3a3db450c80
tuned message: failure can happen towards the end, e.g. due to failed sessions or progress.stopped;
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() })
         }
       }
   }