From aa77afa9d828d0bbb5d6fd5faf2e971b515a19fd Mon Sep 17 00:00:00 2001
From: glondu
Date: Tue, 28 Oct 2008 18:43:16 +0000
Subject: Native "Declare ML Module" when possible

Dynlink.add_{interfaces,available_units} are deprecated and not
implemented natively. Currently, native "Declare ML Module" doesn't
work because of this. Dynlink-related should be switched to the API
introduced in OCaml 3.07.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11518 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 configure | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'configure')

diff --git a/configure b/configure
index d4483fd9db..624f6cf1bc 100755
--- a/configure
+++ b/configure
@@ -455,6 +455,13 @@ if [ "$coq_debug_flag" = "-g" ]; then
     esac
 fi
 
+# Native dynlink
+if test -f `"$CAMLC" -where`/dynlink.cmxa; then
+    HASNATDYNLINK=true
+else
+    HASNATDYNLINK=false
+fi
+
 # Camlp4 / Camlp5 configuration
 
 if [ "$camlp5dir" != "" ]; then
@@ -900,6 +907,7 @@ let camlp4 = "$CAMLP4"
 let camlp4lib = "$ESCCAMLP4LIB"
 let best = "$best_compiler"
 let arch = "$ARCH"
+let has_natdynlink = $HASNATDYNLINK
 let osdeplibs = "$OSDEPLIBS"
 let version = "$VERSION"
 let date = "$DATE"
@@ -985,6 +993,7 @@ sed -e "s|LOCALINSTALLATION|$local|" \
     -e "s|COQIDEOPT|$COQIDE|" \
     -e "s|CHECKEDOUTSOURCETREE|$checkedout|" \
     -e "s|WITHDOCOPT|$with_doc|" \
+    -e "s|HASNATIVEDYNLINK|$HASNATDYNLINK|" \
       "$COQSRC/config/Makefile.template" > "$COQSRC/config/Makefile"
 
 chmod a-w "$COQSRC/config/Makefile"
-- 
cgit v1.2.3