diff options
| author | Enrico Tassi | 2015-04-16 11:07:29 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2015-04-16 11:07:29 +0200 |
| commit | 92e491097dbd7ca610ded20c3c4a3bb978c996eb (patch) | |
| tree | 9eadaf39586c63d85e9470f4ec4c16e0a89930bc | |
| parent | f9580dfa7bc89d0ca4c9d8b69d5f4b42d558234e (diff) | |
configure: fix paths on cygwin
Long story short: Filname.concat and other OCaml provided functions
to be "cross platform" don't work for us for two reasons:
1. their behavior is fixed when one compiles ocaml, not when one runs it
2. the build system of Coq is unix only
What is wrong with 1 is that if one compiles ocaml for windows
without requiring cygwin.dll (a good thing, since you don't need to
have cygwin to run ocaml) then the runtime always uses \
as dir_sep, no matter if you are running ocaml from a cygwin shell.
If you use \ as a dir separaton in cygwin command lines, without
going trough the cygpath "mangler", then things go wrong.
The second point is that the makefiles we have need a unix like
environment (e.g. we call sed). So you can't compile Coq without
cygwin, unless you use a different build system, that is not what
we support (1 build system is enough work already, IMO).
To sum up: Running coq/ocaml requires no cygwin, comipling coq requires
a unix like shell, hence paths shall be unix like in configure/build stuff.
| -rw-r--r-- | configure.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml index 9ff483603c..0169dffa9c 100644 --- a/configure.ml +++ b/configure.ml @@ -27,7 +27,7 @@ let die msg = eprintf "%s\nConfiguration script failed!\n" msg; exit 1 let s2i = int_of_string let i2s = string_of_int -let (/) = Filename.concat +let (/) x y = x ^ "/" ^ y (** Remove the final '\r' that may exists on Win32 *) |