On Fri, Jan 3, 2020 at 11:11 AM Thomas Backlund <tmb@xxxxxxxxxx> wrote:
>
> Does not seem to exist in public git yet, maybe you forgot to push ?
Not "forgot", but I've pulled a couple of other things, and done my
usual build tests etc. I tend batch up the pulls and pushes a bit,
sorry for not making that clear.
But I've pushed it all out now.
Linus
