Re: makeinfo 7.1 misses menu errors

[Gavin Smith]

On Mon, Jan 22, 2024 at 10:50:07PM +0100, pertusus@free.fr wrote:
> 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?

I had in mind at least to set CHECK_NORMAL_MENU_STRUCTURE before the
next release to get the warnings that were output before, if the warnings
cannot be improved.  Perhaps this could change in the future if more manuals
stop using @menu blocks following the "normal" structure.