diff -r 4b014e6c1dfe -r 7799ec03b8bd src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Oct 18 19:05:06 2023 +0200 +++ b/src/Pure/Tools/build.scala Wed Oct 18 19:26:37 2023 +0200 @@ -115,7 +115,7 @@ } def process_options(options: Options, node_info: Host.Node_Info): Options = - Host.process_policy_options(options, node_info.numa_node) + Host.node_options(options, node_info) final def build_store(options: Options, build_hosts: List[Build_Cluster.Host] = Nil,