Re: [gnu-prog-discuss] U+2018 symbol U+2019

[Karl Berry]

    So, I propose to use U+2018 and U+2019 for @code, @file... quotes
    in Info when
     @documentencoding utf-8
    is set and --disable-encoding is not set, consistently with -- 
    --- and `` and '' being turned to Unicode and utf8.

Yes, it is consistent, so let's do it.

Thanks,
k