Re: [doc patch] Move @menu to end of @node (Auto-loading)

[Eli Zaretskii <eliz@gnu.org>]

> Date: Tue, 27 Mar 2012 22:33:21 +0200
> From: Jan Kratochvil <jan.kratochvil@redhat.com>
> 
> info '(texinfo)Menu Location'
> 
> # A menu must be located at the end of a node, without any regular text
> # or additional commands between the `@end menu' and the beginning of the
> # next node.  (As a consequence, there may be at most one menu in a node.)
> # 
> #   This is actually a useful restriction, since a reader who uses the
> # menu could easily miss any such text.  Technically, it is necessary
> # because in Info format, there is no marker for the end of a menu, so
> # Info-reading programs would have no way to know when the menu ends and
> # normal text resumes.
> 
> This is violated at multiple places in gdb.texinfo.  But I see no problem from
> that, info command displays it properly, also tested PDF (no menus) and HTML
> (working menus).
> 
> So maybe I can just drop this patch, the menu looks better in the first part.

It is better to be compliant, so please do commit this.

Thanks.