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