diff options
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/Makefile.build b/Makefile.build index 857cb39142..2c6e73c5a9 100644 --- a/Makefile.build +++ b/Makefile.build @@ -496,9 +496,18 @@ printers: $(DEBUGPRINTERS) tools:: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT) -# coqdep_boot : a basic version of coqdep, with almost no dependencies +# coqdep_boot : a basic version of coqdep, with almost no dependencies. -$(COQDEPBOOT): tools/coqdep_lexer.ml tools/coqdep_common.ml tools/coqdep_boot.ml +# Here it is important to mention .ml files instead of .cmo in order +# to avoid using implicit rules and hence .ml.d files that would need +# coqdep_boot. + +COQDEPBOOTSRC:= \ + tools/coqdep_lexer.mli tools/coqdep_lexer.ml \ + tools/coqdep_common.mli tools/coqdep_common.ml \ + tools/coqdep_boot.ml + +$(COQDEPBOOT): $(COQDEPBOOTSRC) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, -I tools, unix) |