Mathieu Lirzin <m...@gnu.org> writes: > Ricardo Wurmus <ricardo.wur...@mdc-berlin.de> writes: > >> Ah, I see, and someone already pushed the wrong version. The commit >> summary should probably be updated to mention this indentation change. > > I don't think so. The current policy is to silently fix indentation > when doing a significant change.
Oh, okay. Thanks for the correction. ~~ Ricardo
