Skip to content

Commit c64d292

Browse files
committed
Provide assistance in the event of a merge conflict
It's certain that merge conflicts will occur as submitters take time to resolve blocking issues and other submissions are accepted in the meantime. The PR merge will fail in this case. Previously there was no provision for handling merge conflicts. The workflow run just failed at the merge job with no comment from the bot. The goal is for the automated system to work with the submitter as much as possible. Towards this goal, when the merge fails, the bot will now comment to explain the problem and provide a link to a general tutorial for using the GitHub PR merge conflict system. A review is requested from the Tooling Team so that they can assist in the event the user is unable to resolve the merge conflict, or the failure was caused by something else.
1 parent 23c5904 commit c64d292

File tree

1 file changed

+36
-0
lines changed

1 file changed

+36
-0
lines changed

.github/workflows/manage-prs.yml

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -349,6 +349,42 @@ jobs:
349349
You can check the logs from the Library Manager indexer for your library(s) here:
350350
${{ needs.parse.outputs.indexer-logs-urls }}
351351
352+
merge-fail:
353+
needs:
354+
- merge
355+
if: failure()
356+
runs-on: ubuntu-latest
357+
steps:
358+
- name: Comment on merge failure
359+
uses: octokit/request-action@v2.x
360+
env:
361+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
362+
with:
363+
route: POST /repos/{owner}/{repo}/issues/{issue_number}/comments
364+
owner: ${{ github.repository_owner }}
365+
repo: ${{ github.event.repository.name }}
366+
issue_number: ${{ github.event.pull_request.number }}${{ github.event.issue.number }}
367+
body: |
368+
|
369+
Your submission meets all requirements. However, the pull request could not be merged.
370+
371+
Please follow this guide to resolve a merge conflict:
372+
https://docs.github.com/en/github/collaborating-with-issues-and-pull-requests/resolving-a-merge-conflict-on-github
373+
374+
Once that is done, it will be merged automatically.
375+
376+
- name: Request a review in case assistance is required
377+
uses: octokit/request-action@v2.x
378+
env:
379+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
380+
with:
381+
route: POST /repos/{owner}/{repo}/pulls/{pull_number}/requested_reviewers
382+
owner: ${{ github.repository_owner }}
383+
repo: ${{ github.event.repository.name }}
384+
pull_number: ${{ github.event.pull_request.number }}${{ github.event.issue.number }}
385+
team_reviewers: |
386+
- arduino/team_tooling
387+
352388
request-review:
353389
needs:
354390
- enabled

0 commit comments

Comments
 (0)