On Mon, Aug 18, 2014 at 05:37:09PM +0100, Thomas Adam wrote: > 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.
Done. I've moved the old master to master-bak-1. We can delete that and dv/undo-reindent once we're sure we don't need them anymore. Ciao Dominik ^_^ ^_^ -- Dominik Vogt
