Github has been doing this for at least 5 years now. Merging a pull request merges whatever the latest commit on that branch is in the specific backend that handles the merge request. It does not merge what was just pushed into that branch.