[lemoncucumber]

Yeah, `git pull` is just shorthand for `git fetch` followed by `git merge`, so it's technically a superset of a "merge request".

And it also handles the cross-repo case, which is a common case in the Github model of "make your own personal fork of the upstream repo and send PRs from there," which has advantages -- it allows random people to send PRs without needing to give them permission to e.g. pollute the upstream repo's branch namespace.