On Mon, Jan 24, 2022 at 12:35 PM Tobias Burnus <tobias@codesourcery.com> wrote:
>
> Hi H.J.,
>
> On 24.01.22 19:53, H.J. Lu wrote:
> > Try this one.
>
> good news - that patch works with the build script and also with 'make
> install-{html,info,pdf}' :-)
>
I am checking it in.
Thanks.
--
H.J.