diff options
| author | letouzey | 2012-08-07 15:36:16 +0000 |
|---|---|---|
| committer | letouzey | 2012-08-07 15:36:16 +0000 |
| commit | c7365ac4a36e6e7cc90582f38cd6f9adc2d88f1f (patch) | |
| tree | b5ae2786ff62a6e6827dbfb82845cc75fb116182 | |
| parent | 145bd37bb83b41749b7e95f535569c249e98df38 (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
| -rwxr-xr-x | configure | 19 |
1 files changed, 8 insertions, 11 deletions
@@ -450,16 +450,20 @@ fi mk_win_path () { case $ARCH,$CYGWIN in win32,yes) cygpath -m "$1" ;; - win32*) "$ocamlexec" "$COQSRC/tools/mingwpath.ml" "$1" ;; + win32*) "$ocamlexec" "tools/mingwpath.ml" "$1" ;; *) echo "$1" ;; esac } -case $ARCH in +case $ARCH,$src_spec in + win32,yes) echo "Error: the -src option is currently not supported on Windows" + exit 1;; win32) CAMLBIN=`mk_win_path "$CAMLBIN"`;; esac -CAMLVERSION=`"$bytecamlc" -version` +# Beware of the final \r in Win32 +CAMLVERSION=`"$CAMLC" -version | tr -d "\r"` +CAMLLIB=`"$CAMLC" -where | tr -d "\r"` case $CAMLVERSION in 1.*|2.*|3.0*|3.10*|3.11.[01]) @@ -485,13 +489,6 @@ CAMLTAG=OCAML`echo $CAMLVERSION | sed -e "s/\([1-9]\)\.\([0-9]*\).*/\1\2/g"` # For coqmktop & bytecode compiler -case $ARCH in - win32) # Awfull trick to get around a ^M problem at the end of CAMLLIB - CAMLLIB=`"$CAMLC" -where | sed -e 's/^\(.*\)$/\1/'` ;; - *) - CAMLLIB=`"$CAMLC" -where` -esac - if [ "$coq_debug_flag" = "-g" ]; then case $CAMLTAG in OCAML31*|OCAML4*) @@ -1003,7 +1000,7 @@ config_template="$COQSRC/config/Makefile.template" ### since some of them (e.g. $COQSRC) will be escaped escape_string () { - "$ocamlexec" "$COQSRC/tools/escape_string.ml" "$1" + "$ocamlexec" "tools/escape_string.ml" "$1" } # Escaped version of browser command |
