-5. (cd docs/building && make building.ps && ps2pdf building.ps building.pdf)
-6. (cd ghc/docs/set && make set.ps && ps2pdf set.ps set.pdf)
-7. Make License and ANNOUNCE into RTF (or just rename as RTF?).
+5. (cd ghc/docs/set && make set.ps set.html && ps2pdf set.ps set.pdf)
+6. Make License and ANNOUNCE into RTF (or just rename as RTF?).
+
+It also seems necessary to run jadetex once more on the docs before
+turning them into PS. The docs are built correctly under Linux, so I'm
+not sure what goes wrong here.
\ No newline at end of file