build: Support $(DESTDIR).
authorAndre Noll <maan@tuebingen.mpg.de>
Sun, 17 Jul 2016 19:27:12 +0000 (21:27 +0200)
committerAndre Noll <maan@tuebingen.mpg.de>
Sun, 8 Jan 2017 12:58:54 +0000 (13:58 +0100)
commit4f97f4f59172c8d295a22f10204cdef507e3402a
tree01aac11547f889b351893dd2e458badc4751e2c1
parent1426c2f051ddb98b6852cd20b251fd859b0cb253
build: Support $(DESTDIR).

The DESTDIR feature is orthogonal to the existing --prefix option
to configure, and the GNU make manual strongly recommends to support
the feature, so this patch implements it.

The feature works as follows. The content of the DESTDIR make variable
is prepended to each installed target file. It is not set at all in
the Makefile, so files are installed into their expected locations by
default. For example, with the patch applied, one may say

make DESTDIR=/tmp/stage install

to install in /tmp/stage/usr/local.

Other than that, specifying DESTDIR has no effect and the value is
not included in any file contents.
Makefile.real