bug#45143: Incorrect markup in some doc/misc manuals

[Eli Zaretskii]

> From: Richard Stallman <rms@gnu.org>
> Cc: 45143@debbugs.gnu.org
> Date: Fri, 26 Feb 2021 01:32:07 -0500
> 
>   > Of course, no argument here.  My point is that until the Org's Texinfo
>   > export is fixed so that it produces better Texinfo, these problems
>   > will be inevitable.
> 
> The underlying issues have not been addressed, but there are various
> ways to fix this problem.  Protesilaos told me has fixed it,
> and maybe it is fixed -- I am waiting to learn the details.

He fixed them by installing local changes to Org's export as part of
hist manual source in Org.  I suggested that he submits those changes
to Org developers, with the goal of making the official Org Texinfo
export support @kbd etc., and this bring it closer to the goal of
producing higher-quality Texinfo.