On Mon, Aug 18, 2014 at 04:21:18PM +0100, Thomas Adam wrote: > 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?
I've redone the branch from the common base commit 63af0bc172a36ea35f223dce30790ddd5264269a using cherry-pick and manual editing. I've recycled your commit information. The following commits are actually by me but bear the old commit information: 01885bc4172e42d92cb57840674e196d180cb7ef 23e6b9ce70079cd4755e39fe09a15bb0b6e7a9e8 3320850d941ec06ed38e8e5007744c4bf3f103e4 Ciao Dominik ^_^ ^_^ -- Dominik Vogt
