changeset 77318 | 7a03477bf3d5 |
parent 77316 | d17b0851a61a |
child 77368 | 7c57d9586f4c |
--- a/src/Pure/Tools/dump.scala Mon Feb 20 17:13:19 2023 +0100 +++ b/src/Pure/Tools/dump.scala Mon Feb 20 21:04:49 2023 +0100 @@ -97,9 +97,8 @@ skip_base: Boolean = false ): Context = { val session_options: Options = { - val options0 = if (NUMA.available) NUMA.policy_options(options) else options val options1 = - options0 + + NUMA.perhaps_policy_options(options) + "parallel_proofs=0" + "completion_limit=0" + "editor_tracing_messages=0"