handle edge case closing PR in case merge fails due to conflict

vocdoni · Nov 22, 2023 · cb565a2 · cb565a2
1 parent 1550ead
commit cb565a2
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/.github/workflows/verify-contribution.yml b/.github/workflows/verify-contribution.yml
@@ -30,7 +30,8 @@ jobs:
     - name: Merge PR branch
       if: success() && contains(github.event.pull_request.title, 'Contribution:')
       run: |
-        gh pr merge --admin --squash "$PR_URL"
+        gh pr merge --admin --squash "$PR_URL" \
+        || gh pr close -c "Failed, likely another contribution was merged concurrently and yours was lost, please restart your contribution from scratch" "$PR_URL"
       env:
         PR_URL: ${{github.event.pull_request.html_url}}
         GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}