# HG changeset patch
# User wenzelm
# Date 1678725149 -3600
# Node ID f7208db921c200fe261d3c049dce2d8b3a2eee78
# Parent  89fffc5f5728d7e58d16adfb49c387ec716b976c
tuned signature;

diff -r 89fffc5f5728 -r f7208db921c2 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Mon Mar 13 17:30:43 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Mon Mar 13 17:32:29 2023 +0100
@@ -219,7 +219,7 @@
 
     def set_workers(new_workers: State.Workers): State = copy(workers = new_workers)
 
-    def numa_next_node(numa_nodes: List[Int]): (Option[Int], State) =
+    def next_numa_node(numa_nodes: List[Int]): (Option[Int], State) =
       if (numa_nodes.isEmpty) (None, this)
       else {
         val available = numa_nodes.zipWithIndex
@@ -910,7 +910,7 @@
         .make_result(session_name, Process_Result.undefined, output_shasum)
     }
     else {
-      val (numa_node, state1) = state.numa_next_node(build_context.numa_nodes)
+      val (numa_node, state1) = state.next_numa_node(build_context.numa_nodes)
       val node_info = Host.Node_Info(build_context.hostname, numa_node)
 
       progress.echo(