bug#24774: 26.0.50; Menu display navigation commands

[Eli Zaretskii]

> From: Lars Ingebrigtsen <larsi@gnus.org>
> Cc: stephen.berman@gmx.net,  stefan@marxist.se,  24774@debbugs.gnu.org
> Date: Sat, 27 Feb 2021 14:49:14 +0100
> 
> The mean RSS sizes were 61436 and 61465, which is not a noticeable
> difference.

I'm not sure the average is representative here, given the variance.
But anyway, the difference is too small to invest any more energy into
this aspect.