assigned to @htriem
Whatever is to do here, please do it. (separate MR)
Errm... ... forget the separate MR part.
Fixed it, approved & merged
approved this merge request
mentioned in commit 111bb152
merged
