aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-05-23 13:37:51 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-05-23 13:37:51 +0000
commitd05961c7e6cb4a2f8cb70b136f58ef3dee2a9b32 (patch)
treea64d675e49e0f154206204af2cdd70834a1a06c5 /tools
parentf657facaf4fc5c6193acbabd75ef8aaae4674fe7 (diff)
configure: add support of MinGW Win32 environment (fix #2526)
* Since MinGW/Msys doesn't provide a cygpath utility, we emulate it via an ocaml script tools/mingwpath.ml * Avoid the crazy sed portions for backslash escaping, instead use a more robust ocaml script tools/escape_string.ml based on String.escaped * No more config/Makefile.template + sed on it, but rather a "cat << EOF > ..." as for config/coq_config.ml * Normally, support of Cygwin should be preserved, as well as mingw32 cross-compilation from linux (cf. myocamlbuild.ml) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15348 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
-rw-r--r--tools/escape_string.ml1
-rw-r--r--tools/mingwpath.ml15
2 files changed, 16 insertions, 0 deletions
diff --git a/tools/escape_string.ml b/tools/escape_string.ml
new file mode 100644
index 000000000..50e8faada
--- /dev/null
+++ b/tools/escape_string.ml
@@ -0,0 +1 @@
+print_string (String.escaped Sys.argv.(1))
diff --git a/tools/mingwpath.ml b/tools/mingwpath.ml
new file mode 100644
index 000000000..f01b62cce
--- /dev/null
+++ b/tools/mingwpath.ml
@@ -0,0 +1,15 @@
+(** Mingwpath *)
+
+(** Converts mingw-encoded filenames such as:
+
+ /c/Program Files/Ocaml/bin
+
+ to a more windows-friendly form (but still with / instead of \) :
+
+ c:/Program Files/Ocaml/bin
+
+ This nice hack was suggested by Benjamin Monate (cf bug #2526)
+ to mimic the cygwin-specific tool cygpath
+*)
+
+print_string Sys.argv.(1)