Re: makeinfo 7.1 misses menu errors

[pertusus]

On Sun, Jan 21, 2024 at 03:13:25PM -0700, Karl Berry wrote:
> Hi Patrice,
> 
> I understand the principle, but for me the lossage in practice is even
> more unfortunate (by far). It sure seems to me that the "rare" case
> should be the one to have to make the config file setting. Indeed, the
> very fact of making that config file setting would helpfully alert
> contributors and builders that "this is not a normally-structured
> manual".
> 
> I dearly hope you will reconsider. --thanks, karl.

I am not sure that I can change my mind, to me, when there is a doubt,
correctness in principle is more important than usability.  However, I
understand the arguments, which are sound.

Maybe Gavin, you could decide?

-- 
Pat