projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 78a8c33) | patch
don't build gtest in CI (#8323)
authorGereon Kremer <gkremer@cs.stanford.edu>
Thu, 17 Mar 2022 00:37:00 +0000 (01:37 +0100)
committerGitHub <noreply@github.com>
Thu, 17 Mar 2022 00:37:00 +0000 (00:37 +0000)
commitc4d85dde69218b2e4d2d8b1b492701d2ec0d5af2
treefeed58fb1aa708ce7d1fdb23c61d88a447b7e5adtree
parent78a8c3359f21dff0eb214324534b6e85cfaa08a7commit | diff
don't build gtest in CI (#8323)

We currently build gtest in /usr/bin/... with every CI job on ubuntu. This PR removes this and uses our own external project instead. This way, we only build gtest if necessary and then cache these builds with ccache (saving some CI time).
.github/actions/install-dependencies/action.yml diff | blob | history