aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorletouzey2012-10-06 10:08:53 +0000
committerletouzey2012-10-06 10:08:53 +0000
commit4e0def89b221046c6400a3d074b8b2089bd3bced (patch)
treebaa246a16fc5fd9076a0e0e4b510ab0119c4f736
parent0256a92eb0d0265750bd38a85dce4f9487aefe5b (diff)
no need for camlp4 cma's in coq misc tools
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15876 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--Makefile.build13
1 files changed, 7 insertions, 6 deletions
diff --git a/Makefile.build b/Makefile.build
index 0cc9466453..f2fabf918e 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -128,15 +128,16 @@ endif
PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) # works also with new camlp4
+SYSMOD:=str unix
+SYSCMA:=$(addsuffix .cma,$(SYSMOD))
+SYSCMXA:=$(addsuffix .cmxa,$(SYSMOD))
+
ifeq ($(CAMLP4),camlp5)
-SYSMOD:=str unix gramlib
+P4CMA:=gramlib.cma
else
-SYSMOD:=str unix dynlink camlp4lib
+P4CMA:=dynlink.cma camlp4lib.cma
endif
-SYSCMA:=$(addsuffix .cma,$(SYSMOD))
-SYSCMXA:=$(addsuffix .cmxa,$(SYSMOD))
-
###########################################################################
# Infrastructure for the rest of the Makefile
@@ -728,7 +729,7 @@ $(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex
dev/printers.cma: | dev/printers.mllib.d
$(SHOW)'Testing $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(SYSCMA) $^ -o test-printer
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(SYSCMA) $(P4CMA) $^ -o test-printer
@rm -f test-printer
$(SHOW)'OCAMLC -a $@'
$(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@