On Mon, Sep 02, 2024 at 06:12:52PM +0200, Miguel Ojeda wrote: > On Mon, Sep 2, 2024 at 6:09 PM Miguel Ojeda <ojeda@xxxxxxxxxx> wrote: > > > > +if ! command -v "$@" >/dev/null; then > > + echo >&2 "***" > > + echo >&2 "*** pahole '$@' could not be found. pahole will not be used." > > + echo >&2 "***" > > + exit 1 > > +fi > > We may not want to print a warning in this case if this case/setup is > too common, though. yes, I think it's a good idea to skip to remove this one. Kind regards, Nicolas
