From 2861a39461c6e13f701892af84c7beebfb8f4215 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
Date: Wed, 15 Jun 2016 11:33:41 +0200
Subject: 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.
---
 Makefile.build | 10 +++++++++-
 Makefile.ide   |  1 +
 2 files changed, 10 insertions(+), 1 deletion(-)

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
-- 
cgit v1.2.3