fix(Zulip reaction): add emoji_code and realm_emoji for :closed-pr: (…

…#20941) I forgot that for custom emoji, the Zulip API to remove reactions requires also the code and realm_emoji, possibly not both, but certainly at least one!
leanprover-community · Jan 22, 2025 · 3982e7c · 3982e7c
1 parent e0e8605
commit 3982e7c
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/scripts/zulip_emoji_merge_delegate.py b/scripts/zulip_emoji_merge_delegate.py
@@ -107,7 +107,9 @@
             print('Removing closed-pr')
             result = client.remove_reaction({
                 "message_id": message['id'],
-                "emoji_name": "closed-pr"
+                "emoji_name": "closed-pr",
+                "emoji_code": "61282",
+                "reaction_type": "realm_emoji",
             })
             print(f"result: '{result}'")