# HG changeset patch
# User wenzelm
# Date 1690130363 -7200
# Node ID 3153311f0f6c4dfe41e746d82275a08fa3190689
# Parent  126a12483c67e08b60f691776758241daf227402
more robust;

diff -r 126a12483c67 -r 3153311f0f6c src/Pure/Tools/build_cluster.scala
--- a/src/Pure/Tools/build_cluster.scala	Sun Jul 23 14:51:07 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Sun Jul 23 18:39:23 2023 +0200
@@ -288,8 +288,8 @@
   override def rc: Int = synchronized { _rc }
 
   override def close(): Unit = synchronized {
-    _init.foreach(_.cancel())
-    _workers.foreach(_.cancel())
+    _init.foreach(_.join)
+    _workers.foreach(_.join)
     join
     _sessions.foreach(_.close())