Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-06-08 16:51:10 -0700 (Wed, 08 Jun 2005)
Revision: 1129
Log message:
Adjust the double quotes in HTML to look right. We should probably
do it the right way sometime, because of things like this:
\begin{verbatim}
X = $''Hello world''
\end{verbatim}
This will be accidentally changed to:
\begin{verbatim}
X = “Hello world”
\end{verbatim}