# HG changeset patch
# User wenzelm
# Date 1678126157 -3600
# Node ID 28b94fe1c00fc34ad8b2e094f5a3e8f28dce5522
# Parent  1d8a12d1c2e934e08cc6a507edc380fb92d9547e
clarified signature;

diff -r 1d8a12d1c2e9 -r 28b94fe1c00f src/Pure/System/host.scala
--- a/src/Pure/System/host.scala	Mon Mar 06 18:58:48 2023 +0100
+++ b/src/Pure/System/host.scala	Mon Mar 06 19:09:17 2023 +0100
@@ -46,6 +46,16 @@
     } yield n
   }
 
+  def numa_node0(): Option[Int] =
+    try {
+      numa_nodes() match {
+        case ns if ns.length >= 2 && numactl_ok(ns.head) => Some(ns.head)
+        case _ => None
+      }
+    }
+    catch { case ERROR(_) => None }
+
+
 
   /* process policy via numactl tool */
 
@@ -59,18 +69,6 @@
         options.string("process_policy") = if (numactl_ok(node)) numactl(node) else ""
     }
 
-  def perhaps_process_policy(options: Options): Options = {
-    val numa_node =
-      try {
-        numa_nodes() match {
-          case ns if ns.length >= 2 && numactl_ok(ns.head) => Some(ns.head)
-          case _ => None
-        }
-      }
-      catch { case ERROR(_) => None }
-    process_policy(options, numa_node)
-  }
-
 
   /* shuffling of NUMA nodes */
 
diff -r 1d8a12d1c2e9 -r 28b94fe1c00f src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Mon Mar 06 18:58:48 2023 +0100
+++ b/src/Pure/Tools/dump.scala	Mon Mar 06 19:09:17 2023 +0100
@@ -98,7 +98,7 @@
     ): Context = {
       val session_options: Options = {
         val options1 =
-          Host.perhaps_process_policy(options) +
+          Host.process_policy(options, Host.numa_node0()) +
             "parallel_proofs=0" +
             "completion_limit=0" +
             "editor_tracing_messages=0"