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
{{ message }}
This repository has been archived by the owner on Apr 4, 2024. It is now read-only.
Would appreciate confirmation that this is a GitHub issue and not a bors issue.
This PR was merged via bors and the target branch is updated with a merge commit, and the commit (singular) in the branch is now part of the master branch:
If it helps with collecting data points, we've got a self-hosted version of Bors running, and are also seeing this behavior of some PRs staying open after the merge has completed. I just started running our instance with debug logging turned on (hat tip to #1602) and I'm hoping that might reveal more information (if only nothing is happening).
Same here for me. I think github is detecting some non-existing conflicts in the pr and refuses to merge them, even though the PR is actually merged. This is very frustrating.
Would appreciate confirmation that this is a GitHub issue and not a bors issue.
This PR was merged via
bors
and the target branch is updated with a merge commit, and the commit (singular) in the branch is now part of the master branch:However as you can see (as of 8:35am Pacific, 16:35am UTC), the pull request has not been marked merged.
The text was updated successfully, but these errors were encountered: