implement --enable-man-pdfs configure option

implement --enable-man-pdfs configure option

There are now the following behaviors during configure and compilation:

  ./configure --enable-man-pdfs ...
    PDFs of man pages will be generated using ps2pdf. If ps2pdf is not
    installed, pstopdf will be used. If pstopdf is also not installed,
    compilation will fail.

  ./configure --disable-man-pdfs ...
    The build will not check for or attempt to generate any PDF versions of man
    pages. It is irrelevant whether ps2pdf or pstopdf are installed.

  ./configure ... (with neither option)
    If ps2pdf is found in $PATH, PDFs of man pages are generated using ps2pdf.
    If ps2pdf is not found, pstopdf will be looked for and, if found, used to
    generate PDFs of man pages. If neither are found, no PDFs of man pages will
    be generated and compilation will succeed, omitting these.

Closes #1763.