From: Gereon Kremer Date: Thu, 31 Mar 2022 05:59:41 +0000 (+0200) Subject: Only run update-pr for normal commits on main (#8478) X-Git-Tag: cvc5-1.0.0~99 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ed1c57b477c8c0008f858265f117142a061ad94f;p=cvc5.git 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. --- diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index badbcd16c..0e69b32f8 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -137,7 +137,9 @@ jobs: update-pr: runs-on: ubuntu-latest - if: github.repository == 'cvc5/cvc5' && github.event_name == 'push' + if: github.repository == 'cvc5/cvc5' && github.event_name == 'push' && github.ref == 'refs/head/main' + concurrency: + group: update-pr steps: - name: Automatically update PR uses: adRise/update-pr-branch@v0.6.0