Question
Github supports closing Issues from a PR with "Closes" and other keywords. Is it possible to close a Pull Request from a Pull Request?
Background:
I interactively rebased a large PR of mine on br_1 into a more reviewable, merge-able, and semantically useful group of commits on br_2. I opened a second PR from br_2 which should supersede br_1.
The original PR should remain open just in case my reviewer needs to dig into the original development sequence, comments, discussion, etc. Once br_2 is merged, however, the PR on br_1 is no longer useful and should also be closed.
Github's UI seems to indicate that br_2 should close br_1 on merge (see image 1 below), however:
- I have been unable to find this behavior in the documentation
- I was unable to produce this behavior with the following test:
Here, the UI indicates PR#18 will close PR#17.

Here, PR#18 has been merged, but PR#17 did not close.

Is the UI wrong about PR's closing PR's? Am I just missing something here?