Reverting some the index stuff to use tools/newind.py again; this works
better with LaTeX2HTML.

Run pdflatex twice to generate the PDF files, even though LaTeX has already
been run a couple of times.  This ensures that font metrics for the final
run match those for the first run, and seesm to get (somewhat) better
outline results.
1 file changed