projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7e0866c) | patch
Remove dependency on build (#8367)
authorGereon Kremer <gkremer@cs.stanford.edu>
Wed, 23 Mar 2022 03:47:33 +0000 (04:47 +0100)
committerGitHub <noreply@github.com>
Wed, 23 Mar 2022 03:47:33 +0000 (03:47 +0000)
commit740e83760d645080a5edc6b51457c841ad89cb6a
treee960a7a27dd51f52d2feab11fad0bed6aea94845tree
parent7e0866c1c05d06d77c783575d991f75a2da9b59ccommit | diff
Remove dependency on build (#8367)

We automatically update PRs that can be merged automatically in the CI on master. This PR makes it so that this update is done immediately, not only after the CI has run successfully for master.
As we only merge to master if CI works, CI failures on master should only be glitches or issues with the CI itself.
This allows to merge stuff to master twice as fast when using the auto-merge feature.
.github/workflows/ci.yml diff | blob | history