Yes. The default GitHub-recommended workflow of having contributors do `git pull` to integrate their changes an easily result in a confusing spaghetti monster

Yes. The default GitHub-recommended workflow of having contributors do `git pull` to integrate their changes an easily result in a confusing spaghetti monster history even if the contributor only has 1-2 commits that don't merge conflict with anything. For this reason, most major open source projects use that part of the workflow (asking their contributors to rebase their PRs on top of master and never use `git pull --merge`), even if they plan to merge the commits into master via a merge commit. (The Git documentation is very aggressive in discouraging force-pushing of commits, but that advice is intended for a public repository, like the main zulip.git repository, that others might pull from. Obviously, we don't force-push to zulip.git, but if you're using Git right, you should be force-pushing to your fork when you fix a typo in one of your commits.)