aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorletouzey2012-05-15 12:49:49 +0000
committerletouzey2012-05-15 12:49:49 +0000
commit75d56709274a5bcdc94fb26da6843ae0770cc826 (patch)
tree2e6be49cfbcfa90e0a075e446b8caf22ba90010b
parent069561cdbfd1f188908fee5ea020cc44fa1ddfdb (diff)
when cross-compiling with mingw32, let's fix the Filename.dir_sep
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15327 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--myocamlbuild.ml9
-rw-r--r--tools/win32hack.mllib1
-rw-r--r--tools/win32hack_filename.ml4
3 files changed, 14 insertions, 0 deletions
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index dc73cf84c1..7700d9959f 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -402,6 +402,15 @@ let extra_rules () = begin
if w32 then flag ["link"; "ocaml"; "program"; "ide"]
(S [A "-ccopt"; A "-link -Wl,-subsystem,windows"; P w32ico]);
+(** The mingw32-ocaml cross-compiler currently uses Filename.dir_sep="/".
+ Let's tweak that... *)
+
+ if w32 then begin
+ ocaml_lib "tools/win32hack";
+ List.iter (fun (_,s,_) -> tag_file (s^".native") ["use_win32hack"])
+ all_binaries
+ end;
+
(** Coqtop *)
let () =
diff --git a/tools/win32hack.mllib b/tools/win32hack.mllib
new file mode 100644
index 0000000000..42395f65c7
--- /dev/null
+++ b/tools/win32hack.mllib
@@ -0,0 +1 @@
+Win32hack_filename \ No newline at end of file
diff --git a/tools/win32hack_filename.ml b/tools/win32hack_filename.ml
new file mode 100644
index 0000000000..74f70686fe
--- /dev/null
+++ b/tools/win32hack_filename.ml
@@ -0,0 +1,4 @@
+(* The mingw32-ocaml cross-compiler currently uses Filename.dir_sep="/".
+ Let's tweak that... *)
+
+let _ = Filename.dir_sep.[0] <- '\\'