diff options
| author | Pierre Letouzey | 2016-06-15 11:33:41 +0200 |
|---|---|---|
| committer | Pierre Letouzey | 2016-06-15 12:09:25 +0200 |
| commit | 2861a39461c6e13f701892af84c7beebfb8f4215 (patch) | |
| tree | 87b38c6e2e2b85e60da8dcffbf7a6cd4feab1588 | |
| parent | 443a3f3d610d1a6a6fbd3b49a8145863e7ec9f62 (diff) | |
Makefile.build: ensure a build failure in case of a missing rule
Earlier (as in #4812), a target with some declared dependencies (e.g.
in a .d) but no building rule would lead to a successful build,
even though it is actually incomplete.
Side effect: it is now mandatory to declare phony targets in a
.PHONY statement.
| -rw-r--r-- | Makefile.build | 10 | ||||
| -rw-r--r-- | Makefile.ide | 1 |
2 files changed, 10 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index fef1a3f707..2a2eb8796d 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 diff --git a/Makefile.ide b/Makefile.ide index 8d6b5de36f..c50e42341e 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -62,6 +62,7 @@ GTKLIBS=$(shell pkg-config --variable=libdir gtk+-2.0) ########################################################################### .PHONY: coqide coqide-binaries coqide-no coqide-byte coqide-opt coqide-files +.PHONY: ide-toploop # target to build CoqIde coqide: coqide-files coqide-binaries theories/Init/Prelude.vo |