From 2a3523b880c43dd7ce8eedb38334b4d33f639f76 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 15 May 2012 12:49:51 +0000
Subject: 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
---
 ide/ideutils.mli | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'ide/ideutils.mli')

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