diff options
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index fef1a3f70..2a2eb8796 100644 --- a/Makefile.build +++ b/Makefile.build @@ -347,7 +347,7 @@ $(COQC): $(call bestobj, $(COQCCMO)) # other tools ########################################################################### -.PHONY: +.PHONY: tools tools: $(TOOLS) $(OCAMLLIBDEP) $(COQDEPBOOT) # coqdep_boot : a basic version of coqdep, with almost no dependencies. @@ -658,6 +658,14 @@ endif Makefile $(wildcard Makefile.*) config/Makefile : ; +# Final catch-all rule. +# Usually, 'make' would display such an error itself. +# But if the target has some declared dependencies (e.g. in a .d) +# but no building rule, 'make' succeeds silently (see bug #4812). + +%: + @echo "Error: no rule to make target $@ (or missing .PHONY)" && false + # For emacs: # Local Variables: # mode: makefile |