On Aug 21, 2015 8:25 AM, "martin rudalics" <rudalics@gmx.at> wrote:

> I don't have the commit rights. Can you please apply this patch to the
> master?

Pushed as 8c01e88..244a008  master -> master.

Thanks, martin