rustbot sends the same pings multiple times

[RalfJung]

This happens fairly regularly, here's a recent example:

• first ping here, second ping here

I thought rustbot was supposed to remember who already got pinged, and not ping them again when the PR changes?

[RalfJung]

Here's another double-ping: https://github.com/rust-lang/rust/pull/118500