The result of automatic formatting is not perfect, but if someone uses an editor that uses that, it's probably better than nothing. Fixes #15415. [zjs: I resurrected this patch from #11811 and edited the extended comment heavily.]
