On Mon, Aug 18, 2014 at 03:04:19PM +0100, Dominik Vogt wrote: > On Sun, Aug 17, 2014 at 03:30:04PM +0100, Thomas Adam wrote: > > On Sun, Aug 17, 2014 at 03:27:32PM +0100, Dominik Vogt wrote: > > > Would simply reverting the reindentation commit and postponing a > > > new round of reindentation be okay? > > > > Yup; go for it. :) > > Done. The new branch is named dv/undo-reindent. Please double > check that I did not forget to include some files - had to redo > the renaming step from scratch. > > Also, I've added several low level .gitignore files to ignore some > generated files.
Did you actually push your commits onto this branch, as I only see my own butchery there, and nothing from you? -- Thomas Adam
