nicer indentation

This commit is contained in:
Andreas Rumpf 2017-07-11 12:43:32 +02:00
commit 5838271f8b