From ed1c57b477c8c0008f858265f117142a061ad94f Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 31 Mar 2022 07:59:41 +0200 Subject: [PATCH] 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 | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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 -- 2.30.2