push some forgotten formatting changes

This commit is contained in:
Mirek Kratochvil 2019-02-01 10:57:10 +01:00
parent 7c3e802a71
commit 89908fed4a
2 changed files with 6 additions and 6 deletions