diff options
| author | Enrico Tassi | 2020-06-02 14:02:20 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2020-06-02 14:02:20 +0200 |
| commit | db768e6828af62e06eb03d36509be6f8fc1efbf3 (patch) | |
| tree | 243b5182a061de99bb2d585b6712950916a8b641 /stm/asyncTaskQueue.ml | |
| parent | d495815dfc5b4113c2ebcd83b4319dc4dabc3f66 (diff) | |
| parent | 850e3634b91a30a7510fdea9ac970775a79bd64b (diff) | |
Merge PR #12412: Reduce options passed to workers
Ack-by: SkySkimmer
Reviewed-by: gares
Diffstat (limited to 'stm/asyncTaskQueue.ml')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 87d844edb3..a8088dae36 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -130,19 +130,23 @@ module Make(T : Task) () = struct (* Options to discard: 1 argument *) | ( "-async-proofs" | "-vio2vo" | "-o" | "-load-vernac-source" | "-l" | "-load-vernac-source-verbose" | "-lv" - | "-compile" | "-compile-verbose" + | "-require-import" | "-require-export" | "-ri" | "-re" + | "-load-vernac-object" + | "-set" | "-unset" | "-compat" | "-mangle-names" | "-diffs" | "-w" | "-async-proofs-cache" | "-async-proofs-j" | "-async-proofs-tac-j" | "-async-proofs-private-flags" | "-async-proofs-tactic-error-resilience" | "-async-proofs-command-error-resilience" | "-async-proofs-delegation-threshold" | "-async-proofs-worker-priority" | "-worker-id") :: _ :: tl -> set_slave_opt tl + (* Options to discard: 2 arguments *) + | ( "-rifrom" | "-refrom" | "-rfrom" + | "-require-import-from" | "-require-export-from") :: _ :: _ :: tl -> + set_slave_opt tl (* We need to pass some options with one argument *) - | ( "-I" | "-include" | "-top" | "-topfile" | "-coqlib" | "-exclude-dir" | "-compat" - | "-require-import" | "-require-export" | "-require-import-from" | "-require-export-from" - | "-ri" | "-re" | "-rifrom" | "-refrom" | "-load-vernac-object" - | "-w" | "-color" | "-init-file" - | "-profile-ltac-cutoff" | "-main-channel" | "-control-channel" | "-mangle-names" | "-set" | "-unset" - | "-diffs" | "-mangle-name" | "-dump-glob" | "-bytecode-compiler" | "-native-compiler" as x) :: a :: tl -> + | ( "-I" | "-include" | "-top" | "-topfile" | "-coqlib" | "-exclude-dir" + | "-color" | "-init-file" + | "-profile-ltac-cutoff" | "-main-channel" | "-control-channel" + | "-dump-glob" | "-bytecode-compiler" | "-native-compiler" as x) :: a :: tl -> x :: a :: set_slave_opt tl (* We need to pass some options with two arguments *) | ( "-R" | "-Q" as x) :: a1 :: a2 :: tl -> |