Skip to content

Conversation

@bfops
Copy link
Collaborator

@bfops bfops commented Nov 17, 2025

Description of Changes

When a merged PR fails checks, ping the PR author as well.

API and ABI breaking changes

None. CI only.

Expected complexity level and risk

2

Testing

Demo message (not on an actual PR merge):
image

@bfops bfops requested a review from jdetter November 17, 2025 18:00
@bfops bfops marked this pull request as ready for review November 17, 2025 18:00
@bfops bfops added release-any To be landed in any release window no runtime change This change does not affect the final binaries labels Nov 17, 2025
Copy link
Collaborator

@jdetter jdetter left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This seems fine to me, the CI failures are related to the operation was cancelled issue and not related to this PR. I haven't tested anything here but the code looks correct 👍

@bfops bfops added this pull request to the merge queue Nov 17, 2025
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Nov 17, 2025
@bfops bfops added this pull request to the merge queue Nov 17, 2025
@bfops bfops removed this pull request from the merge queue due to a manual request Nov 17, 2025
@bfops bfops enabled auto-merge November 17, 2025 20:26
@bfops bfops added this pull request to the merge queue Nov 17, 2025
Merged via the queue into master with commit 9d57c4d Nov 17, 2025
32 of 36 checks passed
@bfops bfops deleted the bfops/discord-ping branch November 19, 2025 20:49
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

no runtime change This change does not affect the final binaries release-any To be landed in any release window

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants