Open RubyTheRoobster opened 2 years ago
Yes, but unfortunately the bug is in GitHub.
Sometimes, GitHub delivers notifications for events before they "happen". Meaning, it tells the bot that something changed (e.g. a PR has been created), but when the bot asks GitHub for information about the PR, GitHub replies that no such PR exists.
We probably need to add a workaround for this, e.g. sleeping a few seconds to allow GitHub's parts to catch up with themselves.
Issue #23291 was automatically marked as RESOLVED FIXED by the bot when its PR was merged, in addition to a message being posted by the bot about its being merged.
Meanwhile, for issue #23140, the bot mentioned the PR (which targeted stable) being opened, but never posted when the PR was merged, and I had to manually mark it as RESOLVED FIXED. This is clearly a bug.