From 065913e830ea7b01a500c523c47dcbcdab980b72 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 2 Dec 2020 11:08:48 +0100
Subject: [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.
---
 stm/asyncTaskQueue.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'stm/asyncTaskQueue.ml')

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"
-- 
cgit v1.2.3