diff --git a/.github/workflows/zulip_emoji_awaiting_author.yaml b/.github/workflows/zulip_emoji_labelling.yaml similarity index 80% rename from .github/workflows/zulip_emoji_awaiting_author.yaml rename to .github/workflows/zulip_emoji_labelling.yaml index 441218a6aef60b..52fae3a3b3a43b 100644 --- a/.github/workflows/zulip_emoji_awaiting_author.yaml +++ b/.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" diff --git a/scripts/zulip_emoji_merge_delegate.py b/scripts/zulip_emoji_merge_delegate.py index 6af3ff60d60f2e..aa500e87b09bd0 100644 --- a/scripts/zulip_emoji_merge_delegate.py +++ b/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({