Handle deciding what docs to build better

Handle deciding what docs to build better
Now we have variables for whether or not to build the docbook docs as
HTML, as PS, and as PDF. The configure script output now matches what
the build system will do (except it cannot take account of any
mk/build.mk settings, of course).