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)
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

index badbcd16ce4e951d72c953049c5cc004d06dc4cc..0e69b32f8c4b37af556360edca3667b490b77037 100644 (file)
@@ -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