diff options
| author | coqbot-app[bot] | 2020-12-03 20:03:53 +0000 |
|---|---|---|
| committer | GitHub | 2020-12-03 20:03:53 +0000 |
| commit | 88f23b3095c223966352b7d8c2d9990250f0c640 (patch) | |
| tree | 24b25adda4ebac6e0c2b323c9924cf3b9257310a | |
| parent | 632b960ada4392ddd8be6f2e49caab46b93c022f (diff) | |
| parent | 065913e830ea7b01a500c523c47dcbcdab980b72 (diff) | |
Merge PR #13546: [coqide] fix procedure to parse arguments
Reviewed-by: ejgallego
| -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; |