You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
The text was updated successfully, but these errors were encountered: