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. > > ~~ Ricardo
I don't think so. The current policy is to silently fix indentation when doing a significant change. -- Mathieu Lirzin