Tracking of successful mergebot merges #306934
Labels
5. scope: tracking
Long-lived issue tracking long-term fixes or multiple sub-problems
Comments
tomodachi94
added
the
5. scope: tracking
|
Is the bot supposed to be linking successful PRs here? A hacky workaround I've found is to search for "Merge completed". |
|
indeed that should happen, but maybe someone forgot to implement it :D |
This was referenced Aug 25, 2024
This was referenced Aug 26, 2024
Merged
This was referenced Nov 25, 2024
Merged
Merged
Merged
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
analog to #305350 this is the issue to track the successful merges of the mergebot.
The text was updated successfully, but these errors were encountered: