Hi,
On 2023-01-22 22:19:10 +0100, Jelte Fennema wrote:
> Maybe I'm not understanding your issue correctly, but for such
> a case you could push two commits at the same time.
Right.
> Apart from that "git diff -w" will hide any whitespace changes so I'm not I
> personally wouldn't consider it important to split such changes across
> commits.
I do think it's important. For one, the changes made by pgindent et al aren't
just whitespace ones. But I think it's also important to be able to see the
actual changes made in a patch precisely - lots of spurious whitespace changes
could indicate a problem.
Greetings,
Andres Freund