Re: Consistent face for keys in *Help* and `substitute-command-keys'

[Stefan Kangas]

Eli Zaretskii <eliz@gnu.org> writes:

>> The font size is different, yes.
>
> Do we want that to happen in tooltips?

I think so, yes.  If the user has specified :height and we otherwise
respect this face, then why shouldn't we respect also that?

(But the use-case sounds a bit unusual to me, judging by the themes I've
seen: :height is usually changed only for headlines and the like, not
for "body" text.)