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