feat(CI): add emoji to maintainer merge'd PRs also (#24544)

The zulip bot reacts to all label changes, including arbitrary users setting that label. That seems harmless: the emoji is only informational, and the effect of false marking a PR with the label may simply be that it doesn't reviewed as well.

Author: grunweg

…rkflows/zulip_emoji_awaiting_author.yaml …hub/workflows/zulip_emoji_labelling.yaml.github/workflows/zulip_emoji_awaiting_author.yaml renamed to .github/workflows/zulip_emoji_labelling.yaml .github/workflows/zulip_emoji_awaiting_author.yaml renamed to .github/workflows/zulip_emoji_labelling.yaml

@@ -2,8 +2,10 @@ on:
   pull_request:
     types: [labeled, unlabeled]
 jobs:
+  # When a PR is (un)labelled with awaiting-author or maintainer-merge,
+  # add resp. remove the matching emoji reaction from zulip messages.
   set_pr_emoji:
-    if: github.event.label.name == 'awaiting-author'
+    if: github.event.label.name == 'awaiting-author' || github.event.label.name == 'maintainer-merge'
     runs-on: ubuntu-latest
     steps:
     - name: Checkout mathlib repository
@@ -30,5 +32,5 @@ jobs:
         PR_NUMBER: ${{ github.event.number}}
         LABEL_STATUS: ${{ github.event.action }}
       run: |
-        printf $'Running the python script with pr "%s"\n' "$PR_NUMBER"
+        printf $'Running the python script with pr "%s"\n' "$PR_NUMBER" "$LABEL_STATUS"
         python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "$LABEL_STATUS" "$PR_NUMBER"

scripts/zulip_emoji_merge_delegate.py

@@ -72,6 +72,7 @@
     has_bors = any(reaction['emoji_name'] == 'bors' for reaction in reactions)
     has_merge = any(reaction['emoji_name'] == 'merge' for reaction in reactions)
     has_awaiting_author = any(reaction['emoji_name'] == 'writing' for reaction in reactions)
+    has_maintainer_merge = any(reaction['emoji_name'] == 'hammer' for reaction in reactions)
     has_closed = any(reaction['emoji_name'] == 'closed-pr' for reaction in reactions)
     first_in_thread = hashPR.search(message['subject']) and message['display_recipient'] == 'PR reviews' and message['subject'] not in first_by_subject
     first_by_subject[message['subject']] = message['id']
@@ -105,6 +106,13 @@
                 "emoji_name": "merge"
             })
             print(f"result: '{result}'")
+        if has_maintainer_merge:
+            print('Removing maintainer-merge')
+            result = client.remove_reaction({
+                "message_id": message['id'],
+                "emoji_name": "hammer"
+            })
+            print(f"result: '{result}'")
         if has_awaiting_author:
             print('Removing awaiting-author')
             result = client.remove_reaction({
@@ -137,6 +145,12 @@
                 "message_id": message['id'],
                 "emoji_name": "peace_sign"
             })
+        elif 'maintainer-merge' == LABEL:
+            print('adding maintainer-merge')
+            client.add_reaction({
+                "message_id": message['id'],
+                "emoji_name": "hammer"
+            })
         elif LABEL == 'labeled':
             print('adding awaiting-author')
             client.add_reaction({