feat(CI): On bors r/d-, remove ready-to-merge and delegated labels

Author: adomani

.github/workflows/maintainer_bors.yml

@@ -36,12 +36,17 @@ jobs:
           m_or_d="$(printf '%s' "${COMMENT}" |
             sed -n 's=^bors  *\(merge\|r+\) *$=ready-to-merge=p; s=^bors  *d.*=delegated=p' | head -1)"
 
+          remove_labels="$(printf '%s' "${COMMENT}" |
+            sed -n 's=^bors  *\(r\|d\)- *$=remove-labels' | head -1)"
+
           printf $'"bors delegate" or "bors merge" found? \'%s\'\n' "${m_or_d}"
+          printf $'"bors r-" or "bors d-" found? \'%s\'\n' "${remove_labels}"
           printf $'AUTHOR: \'%s\'\n' "${AUTHOR}"
           printf $'PR_NUMBER: \'%s\'\n' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}"
           printf $'%s' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}" | hexdump -cC
 
           printf $'mOrD=%s\n' "${m_or_d}" >> "${GITHUB_OUTPUT}"
+          printf $'removeLabels=%s\n' "${remove_labels}" >> "${GITHUB_OUTPUT}"
           if [ "${AUTHOR}" == 'leanprover-community-mathlib4-bot' ] ||
              [ "${AUTHOR}" == 'leanprover-community-bot-assistant' ]
           then
@@ -87,6 +92,20 @@ jobs:
               --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
           done
 
+      - name: On bors r/d-, remove ready-to-merge or delegated label
+        if: ${{ ! steps.merge_or_delegate.outputs.removeLabels == '' &&
+          steps.user_permission.outputs.require-result == 'true' }}
+        id: remove_labels
+        name: Remove "ready-to-merge" and "delegated"
+        # 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
+        run: |
+          for label in ready-to-merge delegated; do
+            curl --request DELETE \
+              --url "https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}${{ github.event.pull_request.number }}/labels/${label}" \
+              --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
+          done
+
       - name: Set up Python
         if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' &&
           ( steps.user_permission.outputs.require-result == 'true' ||