Browse Source
* Merging revisions r42795 from trunk:
------------------------------------------------------------------------
r42795 | michael | 2019-08-24 11:56:58 +0200 (Sat, 24 Aug 2019) | 1 line
* Small cosmetic improvement to output
------------------------------------------------------------------------
git-svn-id: branches/fixes_3_2@42856 -