diff options
| author | Enrico Tassi | 2020-12-02 11:08:48 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2020-12-03 13:54:05 +0100 |
| commit | 065913e830ea7b01a500c523c47dcbcdab980b72 (patch) | |
| tree | 8e7afce7a6a638a631ef10018c2548eecdebe2fb | |
| parent | db13ff6866731001ad7d3021ab7cb4b3a54cba5c (diff) | |
[coqide] fix procedure to parse arguments
coqide calls coqidetop -batch, if you are in -async-proof on then
coqidetop spawns a worker and passes -batch to it. At some point,
I could not find the commit, this made the worker die.
On linux it seems it works anyway, but on windows this death is
perceived by coqide which then does not start.
| -rw-r--r-- | stm/asyncTaskQueue.ml | 2 | ||||
| -rw-r--r-- | toplevel/workerLoop.ml | 7 |
2 files changed, 2 insertions, 7 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 4f04b9fe1c..4c4c26f47e 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -125,7 +125,7 @@ module Make(T : Task) () = struct "-async-proofs-worker-priority"; CoqworkmgrApi.(string_of_priority priority)] (* Options to discard: 0 arguments *) - | "-emacs"::tl -> + | ("-emacs" | "--xml_format=Ppcmds" | "-batch") :: tl -> set_slave_opt tl (* Options to discard: 1 argument *) | ( "-async-proofs" | "-vio2vo" | "-o" diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml index 1ec55c78c3..59e10b09a0 100644 --- a/toplevel/workerLoop.ml +++ b/toplevel/workerLoop.ml @@ -8,13 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -let rec parse = function - | "--xml_format=Ppcmds" :: rest -> parse rest - | x :: rest -> x :: parse rest - | [] -> [] - let worker_parse_extra ~opts extra_args = - (), parse extra_args + (), extra_args let worker_init init () ~opts = Flags.quiet := true; |