bug#60587: Patch for adding links to symbols' help documentation

[Eli Zaretskii <eliz@gnu.org>]

> From: Drew Adams <drew.adams@oracle.com>
> CC: Eli Zaretskii <eliz@gnu.org>,
>         "60587@debbugs.gnu.org"
> 	<60587@debbugs.gnu.org>,
>         "monnier@iro.umontreal.ca"
> 	<monnier@iro.umontreal.ca>
> Date: Fri, 27 Jan 2023 23:13:36 +0000
> 
> > > 5. Face `info-color' should be named something like
> > > `info-symbol-help-link'.
> > 
> > You're right, `info-color' is too minimalist and not describing what the
> > object represents.
> > 
> > (I dropped it completely because I realised an additional face is
> > redundant since Info distinguishes (slightly) quoted symbols from the
> > text, anyway.)
> 
> I think it's _good_ to have a separate face for this.

I disagree that another face is a Good Thing.  We have too many of
them already.

> That gives users the choice:
> 
> * Have the same appearance for both kinds of link.
> * Have the two kinds of link (Info, *Help*) look
>   different.
> 
> When you provide two faces, users can always customize
> them to look the same, if they like.  Otherwise, they
> don't have that possibility.

The downside of having a separate face is the need to know about it
and customize it separately.  So an additional face is not just an
advantage, it is also a disadvantage.  Thus, we should introduce new
faces only if they really are for a different purpose.  This one
isn't.