diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-11 14:21:40 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-11 14:21:40 +0000 |
| commit | cbe2466edde3811ebeee9da59cba56ab600de39c (patch) | |
| tree | 9e80958dc1185bd043b9d7dee74e6f2da0014dc6 | |
| parent | 547e7ac53d556c1a8036334301c1a707f22b0230 (diff) | |
Prise en compte de l'export des .cmi dans coq_makefile
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11106 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tools/coq_makefile.ml4 | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index a34e21fb5..67f017986 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -158,7 +158,9 @@ let variables l = section "Variables definitions."; print "CAMLP4LIB:=$(shell $(CAMLBIN)camlp5 -where 2> /dev/null || $(CAMLBIN)camlp4 -where)\n"; print "CAMLP4:=$(notdir $(CAMLP4LIB))\n"; - print "COQSRC:=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\ + if Coq_config.local then + (print "COQSRC:=$(COQTOP)\n"; + print "COQSRCLIBS:=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\ -I $(COQTOP)/library -I $(COQTOP)/parsing \\ -I $(COQTOP)/pretyping -I $(COQTOP)/interp \\ -I $(COQTOP)/proofs -I $(COQTOP)/tactics \\ @@ -168,8 +170,11 @@ let variables l = -I $(COQTOP)/contrib/interface -I $(COQTOP)/contrib/jprover \\ -I $(COQTOP)/contrib/omega -I $(COQTOP)/contrib/romega \\ -I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/xml \\ - -I $(CAMLP4LIB)\n"; - print "ZFLAGS:=$(OCAMLLIBS) $(COQSRC)\n"; + -I $(CAMLP4LIB)\n") + else + (print "COQSRC:=$(shell $(COQTOP)coqc -where)\n"; + print "COQSRCLIBS:=-I $(COQSRC)\n"); + print "ZFLAGS:=$(OCAMLLIBS) $(COQSRCLIBS)\n"; if !opt = "-byte" then print "override OPT:=-byte\n" else @@ -188,7 +193,11 @@ let variables l = printf "CAMLOPTLINK:=$(CAMLBIN)ocamlopt -rectypes\n"; print "GRAMMARS:=grammar.cma\n"; print "CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n"; - print "PP:=-pp \"$(CAMLBIN)$(CAMLP4)o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n"; + + (if Coq_config.local then + print "PP:=-pp \"$(CAMLBIN)$(CAMLP4)o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n" + else + print "PP:=-pp \"$(CAMLBIN)$(CAMLP4)o -I . -I $(COQSRC) $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n"); var_aux l; print "\n" |