aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/names.ml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-08-07 15:36:16 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-08-07 15:36:16 +0000
commitc7365ac4a36e6e7cc90582f38cd6f9adc2d88f1f (patch)
treeb5ae2786ff62a6e6827dbfb82845cc75fb116182 /kernel/names.ml
parent145bd37bb83b41749b7e95f535569c249e98df38 (diff)
configure: two minor fixes for win32
* ocamlc -version may end with a \r in win32 (fix #2849) * $COQSRC may initially be cygwin-specific and hence rejected by ocaml. For the moment, an ad-hoc fix is to remove the problematic $COQSRC, and mark the -src option as incompatible with win32... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15696 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/names.ml')
0 files changed, 0 insertions, 0 deletions