Hacker News Reader

But what is the correct git command to ignore all that?

There's no git command to ignore it, the main repo should merge their changes and then the other person can make a PR on the updated changes.

Where are PRs in Git?

Do a git-cherry-pick.