From 9710f18cd53dd2c618fd2b3f92d5854ff46ca806 Mon Sep 17 00:00:00 2001
From: per1234 <accounts@perglass.com>
Date: Mon, 26 Apr 2021 21:26:30 -0700
Subject: [PATCH] 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.
---
 .github/workflows/manage-prs.yml | 36 ++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)

diff --git a/.github/workflows/manage-prs.yml b/.github/workflows/manage-prs.yml
index 02c710cd..3e226e3a 100644
--- a/.github/workflows/manage-prs.yml
+++ b/.github/workflows/manage-prs.yml
@@ -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