I synced and built HEAD right now. It seems to work now after still failing ~10 days ago. So it seems there has been a fix for this during this period. Ciao, Michael.