Closed thejcannon closed 1 month ago
FWIW I've also seen Mergify handle this correctly. So I suspect now it must be a race.
👋 @thejcannon We've opened a ticket internally and we'll look into it ASAP!
Hi @thejcannon
I ran several tests but I can't reproduce the bug. GitHub sends a "pull request closed" event and Mergify dequeues the pull request as expected.
How often do you notice this bug? Did you find any common pattern?
No, seemed like a blip really.
One thing I vaguely remember from bors is that GitHub doesn't retry webhooks. So if you blink and miss it you're SOL. I can go see if GitHub still has the webhooks log and see if any weren't responded to.
Otherwise feel free to close as not reproducible
That'd be a good check. I'll close it in the meantime but feel free to reopen if you see this happening again.
Ah looks like GitHub only stored recent deliveries for the last day-or-so 😭
Steps to Reproduce the Problem
Expected Behavior
The PR is dequeued
Actual Behavior
The PR is forever the head of the queue
Specifications