Fix bad rebase (follow up !314)

I did a too aggressive rebase in !314 (merged) (after the tests were ran) and didn't check carefully enough the diff. This fixes the issue

approved this merge request

/cc @ahennequ @mstahl I'm building locally and will soon merge this. Any test/build started in the last few min until this is merged is not too useful

unassigned @rmatev

merged

mentioned in commit a71e0155

mentioned in issue #128 (closed)

changed title from Fix bad rebase in !314 to Fix bad rebase (follow up !314)

changed the description