diff options
| author |  Enrico Tassi <enrico.tassi@inria.fr> | 2015-04-16 11:07:29 +0200 |
|---|---|---|
| committer | Enrico Tassi <enrico.tassi@inria.fr> | 2015-04-16 11:07:29 +0200 |
| commit | 92e491097dbd7ca610ded20c3c4a3bb978c996eb (patch) | |
| tree | 9eadaf39586c63d85e9470f4ec4c16e0a89930bc /kernel/names.mli | |
| 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.
Diffstat (limited to 'kernel/names.mli')
0 files changed, 0 insertions, 0 deletions