# HG changeset patch
# User wenzelm
# Date 1676889501 -3600
# Node ID 22564364274e16ed9fd9eca94ee1922104248afb
# Parent  f8aa1647d156cd0bc43d72425b0559e381c04c4d
clarified signature;

diff -r f8aa1647d156 -r 22564364274e src/Pure/Tools/build_process.scala
--- 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)