aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rwxr-xr-xconfigure13
1 files changed, 8 insertions, 5 deletions
diff --git a/configure b/configure
index 3d061917c5..232669a7de 100755
--- a/configure
+++ b/configure
@@ -325,12 +325,15 @@ case $CAMLP4VERSION in
echo "Configuration script failed!"
exit 1;;
esac
-case $CAMLP4VERSION,$CAMLOSTYPE in
- 3.04,*)
+case $CAMLP4VERSION in
+ 3.01|3.02|3.03)
+ case $CAMLOSTYPE in
+ Win32) CAMLP4LIB=`"$CAMLP4" -where |sed -e 's|\\\|/|g'`;;
+ *) CAMLP4LIB=`"$CAMLP4" -where`;;
+ esac;;
+ 3.0*)
CAMLP4LIB=+camlp4;;
- *,Win32)
- CAMLP4LIB=`"$CAMLP4" -where |sed -e 's|\\\|/|g'`;;
- *,*)
+ *)
CAMLP4LIB=`"$CAMLP4" -where`;;
esac