Hi Jan!

> Pushed to master with small cosmetic change below.
> 
> Thanks for the patch!

I accidentally sent the wrong patch that missed some things. So sorry. I have
attached a patch with this email to append the previous. Could you please push
it as new commit. Thanks!

Regards,
RG.