diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2020-02-04 07:49:31 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-04 07:49:31 -0800 |
| commit | 4c471e6e99dcd60d07d8978222956dd0ddd151db (patch) | |
| tree | 36a0f450db75f83cc7c9526187b8f9413eecbdb2 | |
| parent | d0f7a3922e38483908d4b86829241a48d8d8db57 (diff) | |
Fix header installation on MacOS. (#3660)
On MacOS sed -i requires a suffix to be set.
| -rwxr-xr-x | src/fix-install-headers.sh | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/fix-install-headers.sh b/src/fix-install-headers.sh index a1f15996a..39d8bc663 100755 --- a/src/fix-install-headers.sh +++ b/src/fix-install-headers.sh @@ -1,5 +1,7 @@ -#!/bin/bash +#!/usr/bin/env bash + +set -e -o pipefail dir=$1 -find "$dir/include/cvc4/" -type f | \ - xargs sed -i 's/include.*"\(.*\)"/include <cvc4\/\1>/' +find "$dir/include/cvc4/" -type f \ + -exec sed -i'' -e 's/include.*"\(.*\)"/include <cvc4\/\1>/' {} + |