# HG changeset patch
# User wenzelm
# Date 1693752247 -7200
# Node ID ca56952b732216c3e42c243ed14bb10c06bf9960
# Parent  28a2c55648d502c68106b128233ed3b596e884ff
proper stop of build_process shutdown, despite errors on workers;

diff -r 28a2c55648d5 -r ca56952b7322 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