4fc1ec09c7
Incidentally, this also closes jvennix-r7#14 (let's see if I can close a PR by merging from another repo!) Also fixes #3782 (opened by accident).