Re: Use variable-pitch face in more places

[Juri Linkov]

> So here's some low-hanging fruit: the header-line and breadcrumb in info.

Thanks, it looks much nicer with variable-pitch.  But the problem is that
before this change the links on the header line were highlighted as links
with blue color, but the patch overwrites all faces with variable-pitch face.
I guess the faces should be merged here, maybe with add-face-text-property?