From: Bruno Haible Date: Thu, 22 Jun 2023 16:30:08 +0000 (+0200) Subject: doc: Use makeinfo option to check menu structure. X-Git-Tag: v1.0~1196 X-Git-Url: https://gitweb.git.savannah.gnu.org/gitweb/?a=commitdiff_plain;h=4dd09a557274d8ec40dc51acdec327f19d107306;p=gnulib.git doc: Use makeinfo option to check menu structure. Trick revealed by Patrice Dumas in . * doc/Makefile (MAKEINFO): Enforce checking of menu structure. --- diff --git a/ChangeLog b/ChangeLog index 8d8229fd69..9e185dad81 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2023-06-22 Bruno Haible + + doc: Use makeinfo option to check menu structure. + Trick revealed by Patrice Dumas in + . + * doc/Makefile (MAKEINFO): Enforce checking of menu structure. + 2023-06-22 Bruno Haible doc: Correct info menu structure. diff --git a/doc/Makefile b/doc/Makefile index e631625d45..8898ff9d3b 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -9,7 +9,9 @@ doc = gnulib lang_env = env LANG= LC_MESSAGES= LC_ALL= LANGUAGE= makeinfo_prog = makeinfo -MAKEINFO = $(lang_env) $(makeinfo_prog) +# The customization variable CHECK_NORMAL_MENU_STRUCTURE is necessary with +# makeinfo versions ≥ 6.8. +MAKEINFO = $(lang_env) $(makeinfo_prog) -c CHECK_NORMAL_MENU_STRUCTURE=1 manual_opts = --no-split --reference-limit=2000 TEXI2HTML = $(MAKEINFO) $(manual_opts) --html