of the HTML documents using the webcheck target.

When there's not a usable .aux file, use mkdvi.sh --aux instead of
building the .dvi completely.  This makes the most difference for the
library reference.