tiny style change [refactoring]

This commit is contained in:
Andreas Rumpf 2019-08-08 18:30:10 +02:00
commit e3c0bf48c5