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? -- Pat
