Should not close pull requests

[SimonSapin]

When a set of builds/tests pass, bors appears to explicitly close the corresponding pull-request. Is there a reason to do this? If it didn’t, GitHub would automatically mark the PR as "Merged" (which is nicer than "Closed") when bors merges into master and the commit ends up in HEAD’s ancestry.

[brson]

Many of the closed Rust PR's say 'merged'.

[SimonSapin]

Maybe there is a race condition between the API call for closing and the push of the merge commit eventually marking the PR as merged?

[SimonSapin]

The above is only speculation, but the source code comments do talk about closing PRs which is at least unnecessary.

[huonw]

It appears to explicitly close it too.

[SimonSapin]

@huonw , yes, just removing that step should work, AFAIU.

[pnkfelix]

is this fixed now? I feel like I see a lot more PR's marked "Merged" rather than "Closed" after bors is done with them?

[huonw]

@pnkfelix it must be an upstream change, since the relevant line is still there.

[adrientetar]

Maybe adding a check on whether PR has status MERGED would do it, relevant doc is here.

[SimonSapin]

Bors may or may not still be closing issues explicitly, but recent PRs seem to be marked by GitHub at "Merged" rather than "Closed". I’m closing this issue as "works for me".

[adrientetar]

@SimonSapin Yea, it seems like a change on GitHub's end makes it changes PRs from Closed to Merged. Still, not closing issues or doing it conditionally looks like a legit enhancement to do imho.

[SimonSapin]

I closed the issue as I personally don’t see this as a problem anymore. Feel free to re-open if you feel differently.

[huonw]

This still happens occasionally rust-lang/rust#12445, rust-lang/rust#12492, rust-lang/rust#12311.