Question about git: What do you do when you have a massive pull request? This guy I work with made a PR with 13k files out of which 11-12k is basically HTML's that should have been added as an initial commit, and remaining ones are actual files that we worked on. Should I ask him to somehow split his work in two parts?

13k files...
1 PR.....

Either this is a new repo for a old project, or someone's linter when nuts?

Break the PR up into "shit that doesn't need reviewing" and "these things we actually changed"

Yes. They should be split into digestible units. Git etiquette dictates it's the PR author's responsibility to respect the time of their teammates. Small, digestible PRs are part of that.

In this particular case, I assume he didn't write most of those himself and they come from some library or other resource. The things that aren't his code, should be blocked into a single assets commit and PR. That makes it easier for you to determine what you need to care about in the review.

@rutee07 that sounds hot, I thought the point was to punish the guy?

I agree with the others, it's the responsibility of the PR creator to respect the reviewer's time. What is even in all those 13k files? Generated shit? How lomg did he work on this?

@rutee07 you make that sound likes it's suppose to be a bad thing 🤷‍♂️you getting bad at this threatening game.

Big PRs happen (I once did a -600_000 +600_000 on a repo with 60 devs)
But generally, 1 script = 1 PR, additional manual changes go in another pr