diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-02-27 14:37:51 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-02-27 14:37:51 +0000 |
| commit | d298481418ca18736180df25bddaf303f5cf7fce (patch) | |
| tree | 8106a76f1f1b298bd7dc55ddcf0a89d656d0b0ae | |
| parent | 8f363f638f4cd1fe86f42e202b9e405676a7b624 (diff) | |
Makefile: avoid building an empty contrib.cmxa
Patch suggested by Yves. Now that the list of contrib to link statically
in coqtop can be empty, we should avoid trying to build an empty
contrib.cmxa, since this fails at least on MacOS.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11947 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile.common | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common index acbc2feaa..620868519 100644 --- a/Makefile.common +++ b/Makefile.common @@ -343,8 +343,11 @@ CONTRIBSTATIC:=\ $(CCCMO) $(FOCMO) $(SUBTACCMO) $(RTAUTOCMO) \ $(FUNINDCMO) +CONTRIBCMA:=contrib/contrib.cma + ifneq ($(HASNATDYNLINK),false) CONTRIBSTATIC:= + CONTRIBCMA:= INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) $(DPCMA) \ $(XMLCMA) $(FUNINDCMA) $(SUBTACCMA) PLUGINS:=$(INITPLUGINS) \ @@ -371,7 +374,7 @@ CMXA:=$(CMA:.cma=.cmxa) LINKCMO:=$(CONFIG) lib/lib.cma kernel/kernel.cma library/library.cma \ pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ parsing/parsing.cma tactics/tactics.cma toplevel/toplevel.cma \ - parsing/highparsing.cma tactics/hightactics.cma contrib/contrib.cma + parsing/highparsing.cma tactics/hightactics.cma $(CONTRIBCMA) LINKCMOCMXA:=$(LINKCMO:.cma=.cmxa) LINKCMX:=$(LINKCMOCMXA:.cmo=.cmx) |