bug#46926: Remove the quotes from highlighted/linked symbols when displaying docs

[Eli Zaretskii]

> Date: Sat, 13 Mar 2021 07:51:11 +0000
> From: scame <laszlomail@protonmail.com>
> Cc: "rms@gnu.org" <rms@gnu.org>, "46926@debbugs.gnu.org" 
> <46926@debbugs.gnu.org>, "larsi@gnus.org" <larsi@gnus.org>, 
> "stefan@marxist.se" <stefan@marxist.se>
> 
> > Since the quotes are present in the original doc strings (and will
> > stay there, for sure), the implementation of your proposal would be to
> > remove them when we generate the "buttons" (a.k.a. "links") for them
> > in the Help buffer. So, if people feel that removing the quotes could
> > be desired by some users, how about making it optional, by default
> > off?
> 
> The aim of this bug to make the default epxerience cleaner.
> 
> In the first place it is not developers who should decide these things,
> but visual designers. E.g. I guess Gnome has some visual designers who
> create the Gnome look. They can be asked, but I'm pretty sure they
> will say the cleaner look is better for users.

That sounds like "my way or the highway" to me.  Not very
constructive, I'm afraid.

Does anyone else here think the compromise I proposed could have some
merit?