# HG changeset patch
# User wenzelm
# Date 1676980402 -3600
# Node ID 1ab68d4370ecffc17ecfc8fea0535cd4bc6cc59a
# Parent  e9beaaf955bfa44b7dd5762f12bdb83ad5aa3c85
tuned signature;

diff -r e9beaaf955bf -r 1ab68d4370ec src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Tue Feb 21 12:50:03 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Tue Feb 21 12:53:22 2023 +0100
@@ -172,6 +172,9 @@
     running: Map[String, Build_Job] = Map.empty,
     results: Map[String, Build_Process.Result] = Map.empty
   ) {
+    def get_numa: (Int, Set[Int]) = (numa_index, numa_running)
+    def put_numa(i: Int): State = copy(numa_index = i)
+
     def finished: Boolean = pending.isEmpty
 
     def remove_pending(name: String): State =
@@ -263,13 +266,12 @@
     val available = build_context.numa_nodes.zipWithIndex
     if (available.isEmpty) None
     else {
-      val used = _state.numa_running
-      val index = _state.numa_index
+      val (index, used) = _state.get_numa
       val candidates = available.drop(index) ::: available.take(index)
       val (n, i) =
         candidates.find({ case (n, i) => i == index && !used(n) }) orElse
         candidates.find({ case (n, _) => !used(n) }) getOrElse candidates.head
-      _state = _state.copy(numa_index = (i + 1) % available.length)
+      _state = _state.put_numa((i + 1) % available.length)
       Some(n)
     }
   }