aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--stm/asyncTaskQueue.ml2
-rw-r--r--toplevel/workerLoop.ml7
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;