Thanks for reporting the issue to github! I've promised to you some time ago to file a bug for this issue, so I did this in the end. I don't think it's worth discussing this with upstream. This guy won't listen to me and won't accept a fix for that issue either. I'm pretty sure.