projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d0f7a39) | patch
Fix header installation on MacOS. (#3660)
authorMathias Preiner <mathias.preiner@gmail.com>
Tue, 4 Feb 2020 15:49:31 +0000 (07:49 -0800)
committerGitHub <noreply@github.com>
Tue, 4 Feb 2020 15:49:31 +0000 (07:49 -0800)
commit4c471e6e99dcd60d07d8978222956dd0ddd151db
tree36a0f450db75f83cc7c9526187b8f9413eecbdb2tree
parentd0f7a3922e38483908d4b86829241a48d8d8db57commit | diff
Fix header installation on MacOS. (#3660)

On MacOS sed -i requires a suffix to be set.
src/fix-install-headers.sh diff | blob | history