aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-06-15 14:13:15 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-06-15 14:13:15 +0000
commit5718d17ed9f8c593048b48bc8826c4715e1048ae (patch)
tree00bb1fd99db87574a9a39db6da245ef97d00e423
parent868ae672f70f7fd6f6c0f91384dcb3a9714997cc (diff)
Report des modifications faites lors de la 8.0pl3 (bis)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8960 85f007b7-540e-0410-9357-904b9bb8a0f7
-rwxr-xr-xconfigure33
1 files changed, 18 insertions, 15 deletions
diff --git a/configure b/configure
index 6e08d08b6..1c91ff30e 100755
--- a/configure
+++ b/configure
@@ -489,16 +489,19 @@ echo ""
# Building the $COQTOP/config/coq_config.ml file
#####################################################
-# damned backslashes under M$Windows
-case $ARCH in
- win32)
- CAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'`
- BINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'`
- LIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'`
- MANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'`
- EMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'`
- ;;
-esac
+# An escaped version of a variable
+escape_var () {
+ocaml 2>&1 1>/dev/null <<EOF
+ prerr_endline(String.escaped(Sys.getenv"$VAR"));;
+EOF
+}
+
+export COQTOP BINDIR LIBDIR CAMLLIB
+ESCCOQTOP="`VAR=COQTOP escape_var`"
+ESCBINDIR="`VAR=BINDIR escape_var`"
+ESCLIBDIR="`VAR=LIBDIR escape_var`"
+ESCCAMLLIB="`VAR=CAMLLIB escape_var`"
+ESCCAMLP4LIB="$ESCCAMLLIB"/camlp4
mlconfig_file=$COQTOP/config/coq_config.ml
rm -f $mlconfig_file
@@ -506,11 +509,11 @@ cat << END_OF_COQ_CONFIG > $mlconfig_file
(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)
let local = $local
-let bindir = "$BINDIR"
-let coqlib = "$LIBDIR"
-let coqtop = "$COQTOP"
-let camllib = "$CAMLLIB"
-let camlp4lib = "$CAMLP4LIB"
+let bindir = "$ESCBINDIR"
+let coqlib = "$ESCLIBDIR"
+let coqtop = "$ESCCOQTOP"
+let camllib = "$ESCCAMLLIB"
+let camlp4lib = "$ESCCAMLP4LIB"
let best = "$best_compiler"
let arch = "$ARCH"
let osdeplibs = "$OSDEPLIBS"