rustbot failed to ping people in a PR

[RalfJung]

In rust-lang/rust#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.

[apiraino]

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)

[RalfJung]

The same happened again in rust-lang/rust#127907: the PR mutates builtin derives, but no ping for that was done on PR creation, nor on the first force-push. The second force-push a few days later then triggered that ping.

(I've seen this more often but I don't always report that here.)

[ehuss]

Which mentions would you have expected those PRs to trigger?