Re: [GIT PULL] nolibc changes for v5.19

[Willy Tarreau]

On Mon, May 23, 2022 at 10:50:43PM +0200, Willy Tarreau wrote:
> On Mon, May 23, 2022 at 01:30:37PM -0700, Linus Torvalds wrote:
> > On Mon, May 23, 2022 at 1:23 PM Willy Tarreau <w@xxxxxx> wrote:
> > >
> > > So I've figured it again. When you run:
> > >
> > >    make tools/help
> > >
> > > you get the help of tools/ commands, [..]
> > 
> > You speak the words, but you don't actually look at what it does.
> > 
> > Try it.
> 
> Why are you saying this ? I've figured the commands by trying
> each of them.

I think I found it:

   make -C tools/ <tool>_<command>

and:

   make tools/<tool>_<command>

work the same on all commands but actually:

   make -C tools/ nolibc_headers

fails while:

   make tools/nolibc_headers

works. I've essentially used the latter by simplicity without noticing
that it doesn't work as suggested with <tool>_install, and I guess
that's what you got.

I'll check why it's like this and will propose a fix.

Thanks,
Willy