Re: cross manual references in html manuals, second

[Karl Berry]

    Maybe other people use it to express another kind of equivalence, but
    it doesn't mean the same thing as ``='' or ``==''.

It is certainly true that == and \equiv (the real symbol, three
horizontal lines) don't mean the same thing.  However, we have to
transliterate \equiv into something for Info.  I think the symbol `=='
is better than the word `equiv', although admittedly it's just my
opinion.  Do you have another suggestion?

Thanks,
karl