etc/options
changeset 77483 291f5848bf55
parent 77390 ff43a524aa5d
child 77603 236e43c8bb5b
--- a/etc/options	Thu Mar 02 15:55:20 2023 +0100
+++ b/etc/options	Thu Mar 02 16:09:22 2023 +0100
@@ -132,6 +132,9 @@
 option timeout_build : bool = true
   -- "observe timeout for session build"
 
+option process_policy : string = ""
+  -- "command prefix for underlying process, notably ML with NUMA policy"
+
 option process_output_tail : int = 40
   -- "build process output tail shown to user (in lines, 0 = unlimited)"
 
@@ -165,9 +168,6 @@
 public option ML_system_apple : bool = true
   -- "prefer native Apple/ARM64 platform (change requires restart)"
 
-public option ML_process_policy : string = ""
-  -- "ML process command prefix (process policy)"
-
 
 section "Build Process"