equal
deleted
inserted
replaced
95 selection: Sessions.Selection = Sessions.Selection.empty, |
95 selection: Sessions.Selection = Sessions.Selection.empty, |
96 pure_base: Boolean = false, |
96 pure_base: Boolean = false, |
97 skip_base: Boolean = false |
97 skip_base: Boolean = false |
98 ): Context = { |
98 ): Context = { |
99 val session_options: Options = { |
99 val session_options: Options = { |
100 val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options |
100 val options0 = if (NUMA.available) NUMA.policy_options(options) else options |
101 val options1 = |
101 val options1 = |
102 options0 + |
102 options0 + |
103 "parallel_proofs=0" + |
103 "parallel_proofs=0" + |
104 "completion_limit=0" + |
104 "completion_limit=0" + |
105 "editor_tracing_messages=0" |
105 "editor_tracing_messages=0" |