Commit 4dd09a557274d8ec40dc51acdec327f19d107306
2023-06-22T18:30:08
doc: Use makeinfo option to check menu structure. Trick revealed by Patrice Dumas <pertusus@free.fr> in <https://lists.gnu.org/archive/html/bug-texinfo/2023-06/msg00015.html>. * doc/Makefile (MAKEINFO): Enforce checking of menu structure.