On 7 Oct 2018, at 7:52 pm, Davide Pesavento <pesa at gentoo.org> wrote: > > Hi, > > 'make -j10 install' fails randomly with the error below, seemingly due > to the fact that mk_distinfo.py runs too early. Do the installation separately... make -j10 make install Phil