K 10
svn:author
V 6
murray
K 8
svn:date
V 27
2001-07-21T03:44:27.000000Z
K 7
svn:log
V 268
Allow NICE_HEADERS to be used in the GEN_INDEX case.

NICE_HEADERS is a set of print-only enhancements, however the HTML
backend is invoked whenever an index is generated, so we should not
touch JADEOPTS directly and should instead modify the .tex-ps target
directly.

END