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.build | |
| 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.build')
| -rw-r--r-- | Makefile.build | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/Makefile.build b/Makefile.build index 872f8e30bd..e776c5ec1e 100644 --- a/Makefile.build +++ b/Makefile.build @@ -478,7 +478,7 @@ bin/coq-parser$(EXE):$(LIBCOQRUN) $(PARSERCMO) bin/coq-parser.opt$(EXE): $(LIBCOQRUN) $(PARSERCMX) $(SHOW)'OCAMLOPT -o $@' $(HIDE)$(OCAMLOPT) -linkall $(OPTFLAGS) -o $@ \ - $(LIBCOQRUN) nums.cmxa $(CMXA) $(PARSERCMX) + $(LIBCOQRUN) $(DYNLINKCMXA) nums.cmxa $(CMXA) $(PARSERCMX) pcoq-files:: $(INTERFACEVO) $(INTERFACERC) @@ -755,12 +755,14 @@ toplevel/mltop.cmx: toplevel/mltop.optml | toplevel/mltop.ml4.ml.d toplevel/mlto ## In other words, the Byte-only code doesn't import a new module. toplevel/mltop.byteml: toplevel/mltop.ml4 # no camlp4deps here $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` -DByte -impl $< > $@ \ + $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` \ + -DByte -DHasDynlink -impl $< > $@ \ || ( RV=$$?; rm -f "$@"; exit $${RV} ) toplevel/mltop.optml: toplevel/mltop.ml4 # no camlp4deps here $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` -impl $< > $@ \ + $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` \ + $(NATDYNLINKDEF) -impl $< > $@ \ || ( RV=$$?; rm -f "$@"; exit $${RV} ) # files compiled with -rectypes |