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?).
+
+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