You've already forked library-registry
mirror of
https://github.com/arduino/library-registry.git
synced 2025-07-28 02:41:51 +03:00
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.
This commit is contained in:
36
.github/workflows/manage-prs.yml
vendored
36
.github/workflows/manage-prs.yml
vendored
@ -338,6 +338,42 @@ jobs:
|
||||
You can check the logs from the Library Manager indexer for your library(s) here:
|
||||
${{ needs.parse.outputs.indexer-logs-urls }}
|
||||
|
||||
merge-fail:
|
||||
needs:
|
||||
- merge
|
||||
if: failure()
|
||||
runs-on: ubuntu-latest
|
||||
steps:
|
||||
- name: Comment on merge failure
|
||||
uses: octokit/request-action@v2.x
|
||||
env:
|
||||
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
|
||||
with:
|
||||
route: POST /repos/{owner}/{repo}/issues/{issue_number}/comments
|
||||
owner: ${{ github.repository_owner }}
|
||||
repo: ${{ github.event.repository.name }}
|
||||
issue_number: ${{ github.event.pull_request.number }}${{ github.event.issue.number }}
|
||||
body: |
|
||||
|
|
||||
Your submission meets all requirements. However, the pull request could not be merged.
|
||||
|
||||
Please follow this guide to resolve a merge conflict:
|
||||
https://docs.github.com/en/github/collaborating-with-issues-and-pull-requests/resolving-a-merge-conflict-on-github
|
||||
|
||||
Once that is done, it will be merged automatically.
|
||||
|
||||
- name: Request a review in case assistance is required
|
||||
uses: octokit/request-action@v2.x
|
||||
env:
|
||||
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
|
||||
with:
|
||||
route: POST /repos/{owner}/{repo}/pulls/{pull_number}/requested_reviewers
|
||||
owner: ${{ github.repository_owner }}
|
||||
repo: ${{ github.event.repository.name }}
|
||||
pull_number: ${{ github.event.pull_request.number }}${{ github.event.issue.number }}
|
||||
team_reviewers: |
|
||||
- arduino/team_tooling
|
||||
|
||||
request-review:
|
||||
needs:
|
||||
- parse
|
||||
|
Reference in New Issue
Block a user