Pull request race condition
Attempting to merge a pull request when someone pushes a commit.
- View the pull request in the web interface
- Commit a change to the branch and push via git
- Click merge on the pull request and attempt to merge and close
The previous commit on the branch is merged, not the latest commit. The branch is thankfully not deleted, but an error message is displayed. The branch then needs to be merged manually using git directly.