> On Nov 18, 2017, at 8:13 AM, Dirk Hohndel <dirk at hohndel.org> wrote: > > Which OS are you on? [...] > I now want to know even more which OS you are building on. And in the meantime I have pushed a commit to fix the bug. Please try again /D