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.
