aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPierre Letouzey2014-01-24 18:44:43 +0100
committerPierre Letouzey2014-01-30 18:36:49 +0100
commit931121ebf1e2a4bfc4abe6ad7c78085b04bab363 (patch)
tree0142d35f5a0d27b994267e570ae8a2e77aa77f2e
parentd6ac933cb34aa0f8dbb7e898596f3cf28c8cc35c (diff)
Get rid of two utility files, obsolete now that configure is a .ml
-rw-r--r--tools/escape_string.ml1
-rw-r--r--tools/mingwpath.ml15
2 files changed, 0 insertions, 16 deletions
diff --git a/tools/escape_string.ml b/tools/escape_string.ml
deleted file mode 100644
index 50e8faadaa..0000000000
--- a/tools/escape_string.ml
+++ /dev/null
@@ -1 +0,0 @@
-print_string (String.escaped Sys.argv.(1))
diff --git a/tools/mingwpath.ml b/tools/mingwpath.ml
deleted file mode 100644
index f01b62ccef..0000000000
--- a/tools/mingwpath.ml
+++ /dev/null
@@ -1,15 +0,0 @@
-(** 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)