do not use mkdvi.sh or mkhtl.sh any more.

This slows down building all versions of the documentation, but if you are
only building one format, it does not matter.