-
Committer:
Bruno Haible
-
Date:
2023-06-22 21:04:24 UTC
-
Revision ID:
git-v1:8f9d2b67b7bbfe20f6ecaa6fce78d1e7d3044c40
Ensure that makeinfo ≥ 6.8 checks the @menu structure.
See <https://lists.gnu.org/archive/html/bug-texinfo/2023-06/msg00015.html>.
* doc/Makefile.in (MAKEINFO): Add option
"-c CHECK_NORMAL_MENU_STRUCTURE=1".