GitLab

Killian Lufau authored Mar 06, 2019 and Julien Muchembled committed Mar 07, 2019

Because there's no way anymore to pass the install prefix via an environment
variable, a new `make-install-extra` option (empty by default) is added so
that `make install` command line can be extended with `DESTDIR=...`.

/reviewed-on !524