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.