diff options
| author | Théo Zimmermann | 2020-05-26 10:44:44 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-26 12:04:56 +0200 |
| commit | c68455771e65ae63be35a7f2b67e0c9931878758 (patch) | |
| tree | fdd582bc38a8b50006e0c50d05ea60faa09b97eb /stm | |
| parent | 2d9988d834804b577d934d1af662f9f8924f9322 (diff) | |
Fix worker handling of command-line options that are already included in initial state.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 1a232ac93a..a8088dae36 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -130,18 +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" + | "-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 -> |