tree c7f62a42d51c91cf37f26a00fe497c014a7c3140
parent 7b8f675bfdb1d924af6a2dcc1f79bda5ace7e886
author Nikolaus Demmel <nikolaus@nikolaus-demmel.de> 1601252069 +0200
committer Nikolaus Demmel <nikolaus@nikolaus-demmel.de> 1601252342 +0200

minor formatting fix (wrongly updated in earlier commit)

Change-Id: I544635fd936cb5b7f7bd9255876641cd5a9590c6