aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
authorEnrico Tassi2020-12-02 11:08:48 +0100
committerEnrico Tassi2020-12-03 13:54:05 +0100
commit065913e830ea7b01a500c523c47dcbcdab980b72 (patch)
tree8e7afce7a6a638a631ef10018c2548eecdebe2fb /toplevel
parentdb13ff6866731001ad7d3021ab7cb4b3a54cba5c (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.
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/workerLoop.ml7
1 files changed, 1 insertions, 6 deletions
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;