--- a/src/Pure/Tools/build_process.scala Mon Feb 20 11:34:31 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Mon Feb 20 11:38:21 2023 +0100
@@ -190,6 +190,8 @@
private var _running = Map.empty[String, Build_Job]
private var _results = Map.empty[String, Build_Process.Result]
+ private def test_pending(): Boolean = synchronized { _pending.nonEmpty }
+
private def remove_pending(name: String): Unit = synchronized {
_pending = _pending.flatMap(entry => if (entry.name == name) None else Some(entry.resolve(name)))
}
@@ -208,8 +210,6 @@
Set.from(for { job <- _running.valuesIterator; i <- job.numa_node } yield i))
}
- private def test_running(): Boolean = synchronized { _pending.nonEmpty }
-
private def stop_running(): Unit = synchronized { _running.valuesIterator.foreach(_.terminate()) }
private def finished_running(): List[Build_Job.Build_Session] = synchronized {
@@ -380,8 +380,8 @@
}
def run(): Map[String, Process_Result] = {
- if (test_running()) {
- while (test_running()) {
+ if (test_pending()) {
+ while (test_pending()) {
if (progress.stopped) stop_running()
for (job <- finished_running()) finish_job(job)