]> Savannah Git Hosting - gnulib.git/commit
doc: Use makeinfo option to check menu structure.
authorBruno Haible <bruno@clisp.org>
Thu, 22 Jun 2023 16:30:08 +0000 (18:30 +0200)
committerBruno Haible <bruno@clisp.org>
Thu, 22 Jun 2023 16:30:08 +0000 (18:30 +0200)
commit4dd09a557274d8ec40dc51acdec327f19d107306
tree5d73c77709d6be3ba2740fc410ca18533b2529aa
parenta97e2d66a8516a15a8a2a3d4d8e2d17ab2c59c50
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.
ChangeLog
doc/Makefile