summaryrefslogtreecommitdiff
path: root/tools/mingwpath.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-08-20 18:27:01 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-08-20 18:27:01 +0200
commite0d682ec25282a348d35c5b169abafec48555690 (patch)
tree1a46f0142a85df553388c932110793881f3af52f /tools/mingwpath.ml
parent86535d84cc3cffeee1dcd8545343f234e7285530 (diff)
Imported Upstream version 8.4dfsgupstream/8.4dfsg
Diffstat (limited to 'tools/mingwpath.ml')
-rw-r--r--tools/mingwpath.ml15
1 files changed, 15 insertions, 0 deletions
diff --git a/tools/mingwpath.ml b/tools/mingwpath.ml
new file mode 100644
index 00000000..f01b62cc
--- /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)