proper stop of build_process shutdown, despite errors on workers;
authorwenzelm
Sun, 03 Sep 2023 16:44:07 +0200
changeset 78639 ca56952b7322
parent 78638 28a2c55648d5
child 78640 5ee978b3c009
proper stop of build_process shutdown, despite errors on workers;
src/Pure/Tools/build_cluster.scala
--- a/src/Pure/Tools/build_cluster.scala	Sun Sep 03 16:19:58 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Sun Sep 03 16:44:07 2023 +0200
@@ -324,7 +324,7 @@
 
   override def close(): Unit = synchronized {
     _init.foreach(_.join)
-    _workers.foreach(_.join)
+    _workers.foreach(_.join_result)
     _sessions.foreach(_.close())
 
     _init = Nil