'fix-install-headers.sh' should respect DESTDIR environment variable (#4978)

When using CMake with Unix Makefiles, one can invoke `make install` as
```
make install DESTDIR=/a/b/c
```
so that the files will be installed into `$DESTDIR$CMAKE_INSTALL_PREFIX` (see the [documentation](https://cmake.org/cmake/help/latest/envvar/DESTDIR.html) for details). This currently doesn't work with the `fix-install-headers.sh` script:
```
[...]
-- Installing: /<<PKGBUILDDIR>>/debian/tmp/usr/include/cvc4/util/integer.h
-- Installing: /<<PKGBUILDDIR>>/debian/tmp/usr/include/cvc4/util/rational.h
find: ‘/usr/include/cvc4/’: No such file or directory
```
Here, `CMAKE_INSTALL_PREFIX` is `/usr` but `DESTDIR` is `/<<PKGBUILDDIR>>/debian/tmp/`.

This commit makes the script consider `DESTDIR` (if it is not set, then `$DESTDIR` will be empty and nothing changes) to fix this issue.

Signed-off-by: Fabian Wolff <fabi.wolff@arcor.de>

diff --git a/src/fix-install-headers.sh b/src/fix-install-headers.sh
index 39d8bc663a6c9bc0ae79a82178deabfe8792e08b..7f9fa5d5bc20b28b2626b7daa1ad43afaa89a6df 100755 (executable)
--- a/src/fix-install-headers.sh
+++ b/src/fix-install-headers.sh
@@ -2,6 +2,7 @@
 
 set -e -o pipefail
 
-dir=$1
+dir="$DESTDIR$1"
+
 find "$dir/include/cvc4/" -type f \
   -exec sed -i'' -e 's/include.*"\(.*\)"/include <cvc4\/\1>/' {} +