Makefile: Fix compilation after header removal.
authorAndre Noll <maan@tuebingen.mpg.de>
Mon, 14 Mar 2022 21:28:27 +0000 (22:28 +0100)
committerAndre Noll <maan@tuebingen.mpg.de>
Wed, 18 May 2022 20:42:40 +0000 (22:42 +0200)
commit3bc858ee0d9b929f4cbca61cf5ed8d3184d0cf78
treeecb47ec39ca703db6a7b0ff40af6a53ea477b7fe
parent329bf73b72eea2c5be1bcbd9a9602c0a8994d0be
Makefile: Fix compilation after header removal.

When switching from an older git version which still contains some
header file to a newer version where it got removed, a .d file remains
in build/deps which lists the no longer existing header file as a
prerequisite. This causes the build to fail because the prerequisite
cannot be created. The problem can be worked around by removing the
stale .d file, for example by running make clean, but this is no real
fix, and is inefficient.

The root of the matter is that .d files depend on their .c counterpart,
but this dependency is not stated anywhere in the Makefile. Thus, we
need a rule for the .d target with the same prerequisites and the same
recipe as the object file target. GNU make supports multiple targets,
but the feature does not seem to work as advertised, regardless of
whether rules with independent targets or rules with grouped targets
(using the &: separator) are employed. Thus we bite the bullet and
use two separate rules.
Makefile.real