tuned signature;
authorwenzelm
Mon, 13 Mar 2023 17:32:29 +0100
changeset 77632 f7208db921c2
parent 77631 89fffc5f5728
child 77633 a65b39fdf8b6
tuned signature;
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(