From: FabianWolff <fabi.wolff@arcor.de>
Date: Tue, 1 Sep 2020 05:44:18 +0000 (+0200)
Subject: 'fix-install-headers.sh' should respect DESTDIR environment variable (#4978)
X-Git-Tag: cvc5-1.0.0~2929
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a276c5259782f867584bdd5e6e5cd50adc3c5dae;p=cvc5.git

'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 39d8bc663..7f9fa5d5b 100755
--- 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>/' {} +