[m-rev.] diff: AADEBUG paper and talk for the web page

[Peter Moulder]

> > +This ``retry'' capability is very useful,

> Do these double quotes work in HTML?
> I forget the HTML syntax for proper double quotes,
> but it's worth double-checking that this is correct.

They aren't converted to curly double quotes as in LaTeX.
They give the desired visual effect with some fonts (particularly on
Un*x systems where this convention is common in flat ASCII text).

HTML4-compliant browsers accept “ / ” ("left double quote")
or “ / ” .  Pre-HTML4 browsers don't accept the named
versions, and may well not support the numerical versions either.

I'd suggest leaving the existing `` / '' and perhaps changing in a
couple of years according to support in widely-used browsers.

pjm.
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------