aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-01-07 14:26:26 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-01-07 14:26:26 +0000
commitccfcc920b2136ab056d676a99618b9f2dde6b78f (patch)
tree15c5a85a7be3fdd883d49639d068cae2ee85f475 /Makefile.common
parentde291a7cf681d0b7107946fa33bc0b524c46c1f2 (diff)
Coqide is not built with coqmktop any more
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13777 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common9
1 files changed, 9 insertions, 0 deletions
diff --git a/Makefile.common b/Makefile.common
index 95063aa2f..9e45758c4 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -29,6 +29,12 @@ CHICKENOPT:=bin/coqchk.opt$(EXE)
BESTCHICKEN:=bin/coqchk.$(BEST)$(EXE)
CHICKEN:=bin/coqchk$(EXE)
+ifeq ($(CAMLP4),camlp4)
+CAMLP4MOD:=camlp4lib
+else
+CAMLP4MOD:=gramlib
+endif
+
ifneq ($(HASNATDYNLINK),false)
DYNLINKCMXA:=dynlink.cmxa
NATDYNLINKDEF:=-DHasDynlink
@@ -213,6 +219,9 @@ LINKCMX:=$(CONFIG:.cmo=.cmx) $(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa)
IDECMA:=ide/ide.cma
+LINKIDE:=$(LINKCMO) $(IDECMA) ide/coqide_main.ml
+LINKIDEOPT:=$(LINKCMX) $(IDECMA:.cma=.cmxa) ide/coqide_main.ml
+
# modules known by the toplevel of Coq
OBJSMOD:=Coq_config $(shell cat $(CORECMA:.cma=.mllib))