bug#39042: 26.3; Undocumented keys for Info mode

[Eli Zaretskii]

> From: Stefan Kangas <stefan@marxist.se>
> Date: Tue, 28 Apr 2020 01:13:11 +0200
> Cc: 39042@debbugs.gnu.org
> 
> Please see the attached patch, where I also suggest to move some menu
> items to submenus.  This cuts down the number of items on the top
> level of the menu to 17 compared to 21 before.  This buys us the space
> to add three separators too.

I think you've sent the wrong patch.

Thanks.