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
