diff options
| author | letouzey | 2012-05-29 09:14:53 +0000 |
|---|---|---|
| committer | letouzey | 2012-05-29 09:14:53 +0000 |
| commit | bf7cfcf92c45af9f559f5bf004e9730d96921850 (patch) | |
| tree | 3f69021619d4731e559076f0616b3566f2ec341f /Makefile.build | |
| parent | bdeccec95e1d018ffb18af9209060a9806d0235a (diff) | |
Makefile: avoid too much exported vars (for win32)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15366 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/Makefile.build b/Makefile.build index bae04da3c6..0c14f2354e 100644 --- a/Makefile.build +++ b/Makefile.build @@ -36,10 +36,12 @@ endif # of include, and they will then be automatically deleted, leading to an # infinite loop. -ALLDEPS=$(addsuffix .d, \ +MLFILES:=$(MLSTATICFILES) $(MLEXTRAFILES) + +ALLDEPS:=$(addsuffix .d, \ $(ML4FILES) $(MLFILES) $(MLIFILES) $(CFILES) $(MLLIBFILES) $(VFILES)) -.SECONDARY: $(ALLDEPS) $(GENFILES) $(GENML4FILES) +.SECONDARY: $(ALLDEPS) $(GENFILES) $(ML4FILES:.ml4=.ml) # NOTA: the -include below will lauch the build of all .d. Some of them # will _fail_ at first, this is to be expected (no grammar.cma initially). @@ -839,6 +841,12 @@ COND_OPTFLAGS= \ HACKMLI = $(if $(wildcard $<i),,-intf-suffix .cmi) +define diff + $(strip $(foreach f, $(1), $(if $(filter $(f),$(2)),,$f))) +endef + +MLWITHOUTMLI := $(call diff, $(MLFILES), $(MLIFILES:.mli=.ml)) + $(MLWITHOUTMLI:.ml=.cmx): %.cmx: %.cmi # for .ml with .mli this is already the case $(MLWITHOUTMLI:.ml=.cmi): %.cmi: %.cmo |