diff options
| author | FabianWolff <fabi.wolff@arcor.de> | 2020-09-01 07:44:18 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-31 22:44:18 -0700 |
| commit | a276c5259782f867584bdd5e6e5cd50adc3c5dae (patch) | |
| tree | 1d9fa12cf9fd1f1cbce64ddb8f3ea2c87a07844a | |
| parent | 9b7f2b6b541f192acf2dc525076a4aa0e995be14 (diff) | |
'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>
| -rwxr-xr-x | src/fix-install-headers.sh | 3 |
1 files changed, 2 insertions, 1 deletions
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>/' {} + |