Only run update-pr for normal commits on main (#8478)
authorGereon Kremer <gkremer@cs.stanford.edu>
Thu, 31 Mar 2022 05:59:41 +0000 (07:59 +0200)
committerGitHub <noreply@github.com>
Thu, 31 Mar 2022 05:59:41 +0000 (05:59 +0000)
commited1c57b477c8c0008f858265f117142a061ad94f
tree19c60bb4622b75ea79dd1dcde5ea5c27d53bf5c1
parent078ea64696c3ce3f7267e7f7bee6fb0158871e1c
Only run update-pr for normal commits on main (#8478)

Doing a release (or generally pushing two commits at the same time) can trigger a race condition in the update-pr action that technically fails the CI workflow. This PR only runs this action for normal commits, in particular it does not run it for releases (which is the common case where we push multiple commits at once). To be sure, it also puts all update-pr jobs into a concurrency group that enforces sequential execution.
.github/workflows/ci.yml