[Merged by Bors] - feat: trigger automated Zulip emojis via bors x command#19371
[Merged by Bors] - feat: trigger automated Zulip emojis via bors x command#19371
bors x command#19371Conversation
PR summary 31616311bfImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
jcommelin
left a comment
There was a problem hiding this comment.
Instead of the current "narrow" in the zulip search, I think we should search for messages that include the PR_NUMBER. That will be a much more efficient zulip search.
|
I removed the |
|
✌️ adomani can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
Changes the way in which emoji reactions to `delegated`, `ready-to-merge` and `merged` are applied in Zulip: instead of running periodically a script to add the reactions, the reactions are now applied at the same time that the label is applied, or when PRs are merged into master.
|
Pull request successfully merged into master. Build succeeded: |
bors x commandbors x command
Changes the way in which emoji reactions to
delegated,ready-to-mergeandmergedare applied in Zulip: instead of running periodically a script to add the reactions, the reactions are now applied at the same time that the label is applied, or when PRs are merged into master.The test PR is #19367: I was using #19367 as PR to test, but the mechanism to apply/remove the labels was simply using
push, since triggering the action with a comment could only be done if the script was already on master.