diff options
| author | glondu | 2008-10-28 18:43:16 +0000 |
|---|---|---|
| committer | glondu | 2008-10-28 18:43:16 +0000 |
| commit | aa77afa9d828d0bbb5d6fd5faf2e971b515a19fd (patch) | |
| tree | 3d7c44f018987d0048b1bcc4e87f88ac806e110b /Makefile.common | |
| parent | 578f31889234edba078e14f4152421123c1bc466 (diff) | |
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
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Makefile.common b/Makefile.common index 1be1d0dfb0..11cac44252 100644 --- a/Makefile.common +++ b/Makefile.common @@ -29,6 +29,11 @@ CHICKENOPT:=bin/coqchk.opt$(EXE) BESTCHICKEN:=bin/coqchk.$(BEST)$(EXE) CHICKEN:=bin/coqchk$(EXE) +ifeq ($(HASNATDYNLINK),true) + DYNLINKCMXA:=dynlink.cmxa + NATDYNLINKDEF:=-DHasDynlink +endif + INSTALLBIN:=install INSTALLLIB:=install -m 644 MKDIR:=install -d |