html: Delete redundant code.
authorBen Pfaff <blp@gnu.org>
Sun, 31 Jan 2010 04:40:30 +0000 (20:40 -0800)
committerBen Pfaff <blp@gnu.org>
Sat, 6 Feb 2010 04:14:19 +0000 (20:14 -0800)
This code was part of an earlier attempt at CSS styling for HTML output.
It does nothing useful, so remove it.


No differences found