diff options
Diffstat (limited to 'Makefile.stage1')
| -rw-r--r-- | Makefile.stage1 | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/Makefile.stage1 b/Makefile.stage1 index a558e3aa61..a60d388fc6 100644 --- a/Makefile.stage1 +++ b/Makefile.stage1 @@ -18,8 +18,6 @@ include Makefile.build .SECONDARY: $(MLFILES:.ml=.ml.d) -include $(MLIFILES:.mli=.mli.d) .SECONDARY: $(MLIFILES:.mli=.mli.d) --include $(MLLIBFILES:.mllib=.mllib.d) -.SECONDARY: $(MLLIBFILES:.mli=.mllib.d) ##Depends upon the fact that all .ml4.d for stage1 files are empty -include $(STAGE1_ML4:.ml4=.ml4.ml.d) .SECONDARY: $(STAGE1_ML4:.ml4=.ml4.ml.d) |