bors merge succeeded and PR still open, though target branch was merged into

[AaronFriel]

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:

• chore: Update gocloud.dev, removing azure-sdk-for-go dep pulumi/pulumi#11963

However as you can see (as of 8:35am Pacific, 16:35am UTC), the pull request has not been marked merged.

[nairb774]

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).

Edit: We are running the latest container if that matters: https://hub.docker.com/layers/borsng/bors-ng/latest/images/sha256-675f61531eedf348829f55991b195fde549adbf75ca4c2eb6be6682cca9f5c71

[MarinPostma]

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.

[duckinator]

Another data point in case it helps: encountered this problem with duckinator/bork#289.

[AaronFriel]

@duckinator looks like the time frame lines up with ~4 days ago. Looks like there was an internal service outage in GitHub?

Since about 3 days ago, I don't think we've seen this since with many subsequent merges.

[duckinator]

Yeah, looks like it roughly lines up with a GitHub service outage. I've not encountered the problem since then, either.