Open RalfJung opened 9 months ago
After you force-pushed pings were fired. I wonder if it was just a spurious hiccup (either on the github end or the triagebot), even though the autoassignment worked (as you correctly point out). Perhaps the triagebot logs might give more insights.
Did something like that happened in the past? (just curious)
In https://github.com/rust-lang/rust/pull/115972 rustbot should have pinged some people due to the files that were changed (
mentions
rules), but somehow that didn't happen. I would understand if it missed the PR entirely due to github not running the hook or whatever, but it did auto-assign a reviewer, so clearly the PR was visible -- it just somehow skipped the part where it is supposed to ping people.