On Fri, Oct 4, 2019 at 11:50 AM Robert Pluim <rpluim@gmail.com> wrote:

> This causes 'make bootstrap' to fail for me, although I have no clue
> why:

Yes, sorry. I see it too. I'll take a look asap.