Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-10-27 09:42:06 -0700 (Wed, 27 Oct 1999)
Revision: 2831
Log message:
HTMLDOC does not like "<PRE><IMG ...></PRE>.
Since in this context <PRE> is unnecessary, I removed it.