Revision ead37a018c807df342b6f397d36313b0ad7c97bb

Committed on 22/06/2021 12:41 pm by pkamps <[email protected]> [GitHub Diff]

Minor code style improvement