Eli Zaretskii <eliz@gnu.org> writes:

> We use it in info.el for the symbols.

Hm...  and there it makes sense to have a different font, perhaps: