summaryrefslogtreecommitdiff
path: root/src/fix-install-headers.sh
diff options
context:
space:
mode:
Diffstat (limited to 'src/fix-install-headers.sh')
-rwxr-xr-xsrc/fix-install-headers.sh7
1 files changed, 5 insertions, 2 deletions
diff --git a/src/fix-install-headers.sh b/src/fix-install-headers.sh
index 7f9fa5d5b..49bade416 100755
--- a/src/fix-install-headers.sh
+++ b/src/fix-install-headers.sh
@@ -4,5 +4,8 @@ set -e -o pipefail
dir="$DESTDIR$1"
-find "$dir/include/cvc4/" -type f \
- -exec sed -i'' -e 's/include.*"\(.*\)"/include <cvc4\/\1>/' {} +
+find "$dir/include/cvc5/" -type f \
+ -exec sed -i'' -e 's/include.*"api\/cpp\/\(.*\)"/include <cvc5\/\1>/' {} +
+
+find "$dir/include/cvc5/" -type f \
+ -exec sed -i'' -e 's/"cvc4_export.h"/<cvc5\/cvc4_export.h>/' {} +
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback