diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-03-12 20:09:35 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-03-12 20:09:35 -0700 |
| commit | 1b8ee921760d15492c0c0492ce6a4da07186699a (patch) | |
| tree | d22810e876b2d9e8a68919ff3ff3b950c5525bf6 /src/fix-install-headers.sh | |
| parent | 093d5ffdfa5c1656309da6b9cbdfbbf28574a8a0 (diff) | |
Fix public headers for make install. (#2856)
This commit fixes make install, which previously copied all public header files to ${CMAKE_INSTALL_PREFIX}/ instead of ${CMAKE_INSTALL_PREFIX}/cvc4.
Further, the old build system modified all #include directives in the installed public header files to use the installed headers, e.g., #include "cvc4_public.h" was changed to #include <cvc4/cvc4_public.h>. Now, after make install the script src/fix-install-headers.sh is executed to change the #include directives accordingly (this should be obsolete with the new C++ API).
Diffstat (limited to 'src/fix-install-headers.sh')
| -rwxr-xr-x | src/fix-install-headers.sh | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/fix-install-headers.sh b/src/fix-install-headers.sh new file mode 100755 index 000000000..a1f15996a --- /dev/null +++ b/src/fix-install-headers.sh @@ -0,0 +1,5 @@ +#!/bin/bash + +dir=$1 +find "$dir/include/cvc4/" -type f | \ + xargs sed -i 's/include.*"\(.*\)"/include <cvc4\/\1>/' |