From a276c5259782f867584bdd5e6e5cd50adc3c5dae Mon Sep 17 00:00:00 2001 From: FabianWolff Date: Tue, 1 Sep 2020 07:44:18 +0200 Subject: [PATCH] 'fix-install-headers.sh' should respect DESTDIR environment variable (#4978) MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit 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: /<>/debian/tmp/usr/include/cvc4/util/integer.h -- Installing: /<>/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 `/<>/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 --- src/fix-install-headers.sh | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 /' {} + -- 2.30.2