- Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).

- Added dependency of mltop.ml4 into config/Makefile (see bug #2023).
- Fixed bug #1963 (dependent inversion building a universe-ill-formed
  conversion problem).
- Incidentally, moved "Large non-propositional inductive ..." error
  message to standard himsg.ml error displayer.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11774 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 1 deletions

diff --git a/configure b/configure
index df2b39551..e1b17a64f 100755
--- a/configure
+++ b/configure
@@ -445,7 +445,12 @@ fi
 
 # Native dynlink
 if [ "$natdynlink" = "yes" -a -f `"$CAMLC" -where`/dynlink.cmxa ]; then
-    HASNATDYNLINK=true
+    case `uname -s`,`uname -r`,$CAMLVERSION in
+        Darwin,9.*,3.11.0)  # ocaml 3.11.0 dynlink on MacOS 10.5 is buggy
+            HASNATDYNLINK=false;;
+        *)
+            HASNATDYNLINK=true;;
+    esac
 else
     HASNATDYNLINK=false
 fi