On Mon, Aug 18, 2014 at 05:27:39PM +0100, Dominik Vogt wrote: > 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
Ah, of course. Thanks. That makes sense. I don't think you've missed anything. If you're happy with this, feel free to push it to master. -- Thomas Adam
