aboutsummaryrefslogtreecommitdiff
path: root/stm/workerLoop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'stm/workerLoop.ml')
-rw-r--r--stm/workerLoop.ml6
1 files changed, 5 insertions, 1 deletions
diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml
index 56fcf8537f..50b42512cb 100644
--- a/stm/workerLoop.ml
+++ b/stm/workerLoop.ml
@@ -6,9 +6,13 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-let rec parse args = args
+let rec parse = function
+ | "--xml_format=Ppcmds" :: rest -> parse rest
+ | x :: rest -> x :: parse rest
+ | [] -> []
let loop init args =
+ let args = parse args in
Flags.make_silent true;
init ();
CoqworkmgrApi.init !Flags.async_proofs_worker_priority;