bug#3516: 23.0.94; function key names in Info

[Eli Zaretskii]

> From: "Drew Adams" <drew.adams@oracle.com>
> Cc: <larsi@gnus.org>, <3516@debbugs.gnu.org>
> Date: Tue, 12 Jul 2011 14:03:19 -0700
> 
> >   To end a line, press the <RET> key.
> 
> It's fine, as shorthand for "press the key named <RET>".
> <RET> is the name of the key.
> 
> But it is also fine to write "press `<RET>'".

So we are taking the former view and using just <RET>.

> Thank you.  Now please go DTRT.  That's what this bug report is about.

I don't see any bug, so there's no RTTD except leave the bug report
closed.  I asked for specific pointers to where the usage is
incorrect, but you declined (in so many words).  So that's it.