Manually merging master

I broke your PR by a commit of mine that requires a manual merge. I did it for you :-) Sorry about that!