bug#24597: 25.1; Fonts used by default in Info

[Drew Adams]

> > Why use, by default, two **slightly** different looking fonts?  They are
> > not different enough to make ‘...’ very noticeable.  Nor are they the
> > same.  What's the point of this choice?
> 
> The point is exactly to have a different face for symbols.

I don't disagree with that point.

What's the point of using family Courier for one and Courier New for
the other?  That's the question.  Doesn't seem like a great choice.