3 files changed, 17 insertions, 0 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index e0da0c3dc..b993cfe0e 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -99,6 +99,7 @@ let check_remaining_opt arg =
 let rec filter_coq_opts args =
   let argstr = String.concat " " (List.map Filename.quote args) in
   let cmd = Filename.quote (coqtop_path ()) ^" -nois -filteropts " ^ argstr in
+  let cmd = requote cmd in
   let filtered_args = ref [] in
   let errlines = ref [] in
   try
@@ -146,6 +147,7 @@ let check_connection args =
   let lines = ref [] in
   let argstr = String.concat " " (List.map Filename.quote args) in
   let cmd = Filename.quote (coqtop_path ()) ^ " -batch " ^ argstr in
+  let cmd = requote cmd in
   try
     let ic = Unix.open_process_in cmd in
     lines := read_all_lines ic;
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 9350c765c..f52ef36fc 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -275,9 +275,17 @@ let rec print_list print fmt = function
   | [x] -> print fmt x
   | x :: r -> print fmt x; print_list print fmt r
 
+(* In win32, when a command-line is to be executed via cmd.exe
+   (i.e. Sys.command, Unix.open_process, ...), it cannot contain several
+   quoted "..." zones otherwise some quotes are lost. Solution: we re-quote
+   everything. Reference: http://ss64.com/nt/cmd.html *)
+
+let requote cmd = if Sys.os_type = "Win32" then "\""^cmd^"\"" else cmd
+
 (* TODO: allow to report output as soon as it comes (user-fiendlier
    for long commands like make...) *)
 let run_command f c =
+  let c = requote c in
   let result = Buffer.create 127 in
   let cin,cout,cerr = Unix.open_process_full c (Unix.environment ()) in
   let buff = String.make 127 ' ' in
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 91681d297..c433d92ac 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -73,3 +73,10 @@ val pbar : GRange.progress_bar
   returns an absolute filename equivalent to given filename
 *)
 val absolute_filename : string -> string
+
+(* In win32, when a command-line is to be executed via cmd.exe
+   (i.e. Sys.command, Unix.open_process, ...), it cannot contain several
+   quoted "..." zones otherwise some quotes are lost. Solution: we re-quote
+   everything. Reference: http://ss64.com/nt/cmd.html *)
+
+val requote : string -> string