more robust;
authorwenzelm
Sun, 23 Jul 2023 18:39:23 +0200
changeset 78441 3153311f0f6c
parent 78440 126a12483c67
child 78442 c38aebdf1a3d
more robust;
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())