Handle submission merge failures caused by outdated fork

The automatically generated access token provided by `${{ secrets.GITHUB_TOKEN }}` is used to automatically merge
submission pull requests if they are compliant with all requirements.

If the pull request's branch is behind the parent repository and the code of any GitHub Actions workflow has been
modified in the parent since that time, the token permissions are downgraded, which causes the GitHub API request for
merging the PR to fail with a 403 status.

Previously, this was treated as an unexpected merge failure caused by some problem not resolvable by the PR author. Since
the PR author can easily resolve the failure by bringing their branch up to date (even through the GitHub web interface),
the "Manage PRs" workflow is hereby changed to provide instructions for doing so.

As before, a review will be requested from the maintainer of this repository so that they can monitor the situation and
provide the PR author with assistance if needed.

.github/workflows/manage-prs.yml

@@ -444,7 +444,7 @@ jobs:
 
       - name: Merge pull request
         id: merge
-        continue-on-error: true # Error on merge conflict is expected
+        continue-on-error: true # Error in some situations (e.g., merge conflict) is expected
         uses: octokit/request-action@v2.x
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
@@ -504,6 +504,25 @@ jobs:
     if: needs.merge.outputs.pass == 'false'
     runs-on: ubuntu-latest
     steps:
+      - name: Comment on merge fail due to out of sync PR head branch causing downgraded token
+        if: needs.merge.outputs.status == '403'
+        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: |
+            |
+            ${{ env.ERROR_MESSAGE_PREFIX }}Your submission meets all requirements. However, the pull request could not be merged.
+
+            Please follow this guide to sync your fork:
+            https://docs.github.com/en/github/collaborating-with-pull-requests/working-with-forks/syncing-a-fork
+
+            Once that is done, it will be merged automatically.
+
       - name: Comment on merge conflict
         if: needs.merge.outputs.status == '405'
         uses: octokit/request-action@v2.x
@@ -539,6 +558,7 @@ jobs:
 
       - name: Fail on unidentified merge failure
         if: >
+          needs.merge.outputs.status != '403' &&
           needs.merge.outputs.status != '405' &&
           needs.merge.outputs.status != '409'
         run: exit 1 # Trigger the `unexpected-fail` job