Hi, On Fri, Nov 04, 2016 at 10:34:46PM +0100, Denys Vlasenko wrote: > This seems to be fixed already? > > commit 85100a7067a51c5e6720c0a738317cc2144ab219 > Author: Denys Vlasenko <vda.linux at googlemail.com> > Date: Wed Oct 12 20:56:46 2016 +0200 Yeah, sorry, I had forgotten to refresh the master branch. A.