Pull request race condition

Issue #8446 invalid
Kevin Campbell
created an issue

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.

Comments (2)

  1. Daniel Bennett staff

    Pull requests currently do not auto-update in the event of a simple push (it will when a push includes a merge, or deletion of the underlying branch). When a new commit is pushed, a notification will appear at the top of the page indicating that an update is needed. Until that notification is displayed, seen and acted on, or some other actor updates the pull request, the PR will always refer to the same hash regardless of the state of the underlying branch.

  2. Log in to comment