diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-15 12:49:51 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-15 12:49:51 +0000 |
commit | 2a3523b880c43dd7ce8eedb38334b4d33f639f76 (patch) | |
tree | dcf2207a6cddcd2423e8e61915e9e5c1976f8471 | |
parent | 75d56709274a5bcdc94fb26da6843ae0770cc826 (diff) |
Coqide: in win32 command given to cmd.exe should be more quoted
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15328 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | ide/coq.ml | 2 | ||||
-rw-r--r-- | ide/ideutils.ml | 8 | ||||
-rw-r--r-- | ide/ideutils.mli | 7 |
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 |