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.