Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Do not manually close a pull request
Because of the manual closing, the pull request is occasionally set to "closed" rather than "merged" even though it was successful. This is because there is a little latency between the fast-forwarding and the automatic transition to "merged". If a bad thing happens, it would be better to leave it "open".
- Loading branch information