feat(CI): manage merge-conflict label on push (#20961)

Add a step to the PR summary workflow that adds or removes the `merge-conflict` label, as appropriate.

We place the action in the PR summary workflow, since that workflow already checks out the whole repository, so the "cost" of the step is simply to verify whether there are merge conflicts and add/remove the label.

See #19464 for a PR whose `merge-conflict` label was removed by this workflow.

.github/workflows/PR_summary.yml

@@ -14,6 +14,27 @@ jobs:
       with:
         fetch-depth: 0
 
+    - name: Update the merge-conflict label
+      run: |
+        printf 'PR number: "%s"\n' "${{ github.event.pull_request.number }}"
+        if git merge origin/master --no-ff --no-commit
+        then
+          git merge --abort || true
+          echo "This PR does not have merge conflicts with master."
+          # we use curl rather than octokit/request-action so that the job won't fail
+          # (and send an annoying email) if the labels don't exist
+          curl --request DELETE \
+            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels/merge-conflict \
+            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
+        else
+          echo "This PR has merge conflicts with main."
+          # we use curl rather than octokit/request-action so that the job won't fail
+          # (and send an annoying email) if the labels don't exist
+          curl --request POST \
+            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels/merge-conflict \
+            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
+        fi
+
     - name: Set up Python
       uses: actions/setup-python@v5
       with: