aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-06-15 11:33:41 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-06-15 12:09:25 +0200
commit2861a39461c6e13f701892af84c7beebfb8f4215 (patch)
tree87b38c6e2e2b85e60da8dcffbf7a6cd4feab1588
parent443a3f3d610d1a6a6fbd3b49a8145863e7ec9f62 (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.build10
-rw-r--r--Makefile.ide1
2 files changed, 10 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
diff --git a/Makefile.ide b/Makefile.ide
index 8d6b5de36..c50e42341 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