Just before#842 was merged but 15 minutes later git is still a commit behind and the change wasn't fetched.

I've pulled the change now automatically.

Can we check if this still works?