Re: Conversion of ``quotes''

[Karl Berry]

    > That's because menu lines are rendered with a fixed-size typeface.

    Sorry, I don't understand.

Eli meant within the implementation.  makeinfo attempts to keep track of
when it's in a typewriter-like environment (@example) where '' should
not be converted to ", and when it's in regular text where such
conversions should take place.

    My point is that a literal ``'' looks really ugly (except in certain
    old broken X fonts).  

I'm not sure I agree with your characterization as "broken", but that's
beside the point :).

    So converting them to "" is clearly the right
    thing, but this isn't done in menu lines.

I agree it should be done, but it is not easy to do.  I'll take a look
when I can.

Thanks for the suggestion.

karl