diff options
Diffstat (limited to 'src/fix-install-headers.sh')
| -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>/' {} + |