# HG changeset patch
# User wenzelm
# Date 1676285615 -3600
# Node ID 12fd873af77cc2c0361ca9c82df2f6fe2da5d6bf
# Parent  c7d893278aec7dea66a7a97a9cb5a28a31b839ff
clarified signature: proper scope of synchronized operation;

diff -r c7d893278aec -r 12fd873af77c src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Mon Feb 13 11:35:46 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Mon Feb 13 11:53:35 2023 +0100
@@ -185,8 +185,9 @@
       .nextOption()
   }
 
-  private def used_node(i: Int): Boolean = synchronized {
-    _running.valuesIterator.exists(job => job.numa_node.isDefined && job.numa_node.get == i)
+  private def next_numa_node(): Option[Int] = synchronized {
+    _numa_nodes.next(used =
+      Set.from(for { job <- _running.valuesIterator; i <- job.numa_node } yield i))
   }
 
   private def session_finished(session_name: String, process_result: Process_Result): String =
@@ -317,7 +318,7 @@
           command_timings = build_context(session_name).old_command_timings)
 
       synchronized {
-        val numa_node = _numa_nodes.next(used_node)
+        val numa_node = next_numa_node()
         val job =
           new Build_Job(progress, session_background, store, do_store,
             resources, session_setup, input_heaps, numa_node)