Re: makeinfo 7.1 misses menu errors

[Karl Berry]

Patrice: sure, I understand.

Gavin: let me add one more point: if the warning is not reenabled by
default, you are essentially forcing every maintainer of every manual to
add a new flag to their makeinfo invocation, conditional on the makeinfo
version. This seems ... bad. --thanks, karl.