Re: proposal to remove AVOID_MENU_REDUNDANCY

[Gavin Smith]

On Sun, Mar 31, 2024 at 10:13:03PM +0200, Patrice Dumas wrote:
> Hello,
> 
> I propose to remove the HTML customization variable
> AVOID_MENU_REDUNDANCY:
> 
>  If set, and the menu entry and menu description are the
>  same, then do not print the menu description; default false.
> 
> It seems to me to be for a case that should never happen, is not really
> important, and my wild guess is that nobody uses it.
> 
> Comments?

I'm happy for it to be removed.  It seems that the user can easily
avoid this by leaving the menu description blank.