make Makefile robust against deleted headers

[r28176]

diff --git a/Makefile b/Makefile
index ecc9e6b..8277cf3 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -39,6 +39,11 @@ VPATH = $(srcdir)
 .PHONY: all
 all: firm
 
+# This rule is necessary so that make does not abort if headers get deleted
+# (the deleted header might still be referenced in a .d file)
+%.h:
+       @:
+
 # A very naive way to create a config.h if it is missing
 $(srcdir)config.h:
        @echo MakeConfig $@