Do you mind, Stefano, that I create a merge request on your behalf?
mentioned in commit 36a8188a
Status changed to merged