Clean up whitespace a bit

This commit is contained in:
Peter Eisentraut 2019-07-04 12:31:08 +02:00
parent cfc40d384a
commit dedb6e0143
1 changed files with 14 additions and 14 deletions