tuned signature;

--- a/src/Pure/System/host.scala	Mon Mar 06 19:13:27 2023 +0100
+++ b/src/Pure/System/host.scala	Mon Mar 06 19:18:53 2023 +0100
@@ -32,6 +32,9 @@
   sealed case class Node_Info(hostname: String, numa_node: Option[Int]) {
     override def toString: String =
       hostname + if_proper(numa_node, "/" + numa_node.get.toString)
+
+    def process_policy(options: Options): Options =
+      Host.process_policy(options, numa_node)
   }
 
 

--- a/src/Pure/Tools/build_job.scala	Mon Mar 06 19:13:27 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Mon Mar 06 19:18:53 2023 +0100
@@ -119,7 +119,7 @@
     def job_name: String = session_name
 
     private val info: Sessions.Info = session_background.sessions_structure(session_name)
-    private val options: Options = Host.process_policy(info.options, node_info.numa_node)
+    private val options: Options = node_info.process_policy(info.options)
 
     private val session_sources =
       Sessions.Sources.load(session_background.base, cache = store.cache.compress)