aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/coq.ml9
1 files changed, 8 insertions, 1 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index 8ecdf9caa..0fe831ab3 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -366,7 +366,14 @@ let bind_self_as f =
(** This launches a fresh handle from its command line arguments. *)
let spawn_handle args respawner feedback_processor =
let prog = coqtop_path () in
- let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: "on" :: "-ideslave" :: args) in
+ let async_default =
+ (* disable async processing by default in Windows *)
+ if List.mem Sys.os_type ["Win32"; "Cygwin"] then
+ "off"
+ else
+ "on"
+ in
+ let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: async_default :: "-ideslave" :: args) in
let env =
match !Flags.ideslave_coqtop_flags with
| None -> None