Hi,

The PR looks OK to merge. I'm going to push it on next Friday if nobody has any objections.