Sorry if I misread your message.

All the best

MA


On Tue, May 7, 2024, 19:38 Tomas Hlavaty <tom@logand.com> wrote:

> On Tue 07 May 2024 at 19:10, Marco Antoniotti <marco.antoniotti@unimib.it>
> wrote:
> > pardon me, but
> >
> >       grep type....
> >
> > would yield many more hits
>
> yes, it is always possible to find even worse name to grep
>
> > , and I do not understand why this is relevant to the issue.
>
> don't you search source code?
>
> I just pointed out that your suggested name could be even better.
>
> > The points are two:
>
> I understand that and agree with you.
>
> I just sent to you links to the discussion.
>