diff options
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: |