diff options
| author | letouzey | 2010-03-04 16:18:21 +0000 |
|---|---|---|
| committer | letouzey | 2010-03-04 16:18:21 +0000 |
| commit | 2a0b8d89809fdfd48274359c15ba16d98df95a00 (patch) | |
| tree | 42bcca205f16e6d76e0132f610545ec2fb999bed /Makefile.stage2 | |
| parent | b1edecb1b38df8a88552aa4251982238b3c3125d (diff) | |
Makefile: cleanup of variables containing lists of files, such as MLFILES
- We clarify their definition via some custom make function: find, diff...
- We avoid duplications via some $(sort ...)
- Some name changes:
* old $(MLFILES) now corresponds to $(MLSTATICFILES) (but .ml from
.mly and .mll aren't in it anymore).
* new $(MLFILES) contains all .ml, either static or generated from
.mly .mll .ml4 or _mod.ml made out of .mllib
* $(ML4FILESML) is now $(GENML4FILES)
...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12836 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.stage2')
| -rw-r--r-- | Makefile.stage2 | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/Makefile.stage2 b/Makefile.stage2 index a7ecddc13e..e6a61b8e44 100644 --- a/Makefile.stage2 +++ b/Makefile.stage2 @@ -9,14 +9,13 @@ include Makefile.stage1 include Makefile.doc --include $(MLLIBFILES:.mllib=.mllib.d) -.SECONDARY: $(MLLIBFILES:.mllib=.mllib.d) --include $(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml.d)) -.SECONDARY: $(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml.d)) --include $(ML4FILES:.ml4=.ml.d) -.SECONDARY: $(ML4FILES:.ml4=.ml.d) --include $(VFILES:.v=.v.d) -.SECONDARY: $(VFILES:.v=.v.d) +STAGE2_DEPS := $(addsuffix .d, $(GENPLUGINSMOD) $(GENML4FILES) $(VFILES)) + +.SECONDARY: $(STAGE2_DEPS) +-include $(STAGE2_DEPS) + +# NB: all $(STAGE1_DEPS) are already included thanks to the inclusion of +# Makefile.stage1 # For emacs: # Local Variables: |