1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
Description: The fix-install-headers.sh script doesn't work with DESTDIR
Author: Fabian Wolff <fabi.wolff@arcor.de>
Forwarded: https://github.com/CVC4/CVC4/pull/4978
Last-Update: 2020-08-31
---
This patch header follows DEP-3: http://dep.debian.net/deps/dep3/
--- 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>/' {} +
|
