-# Check whether --enable-html-doc or --disable-html-doc was given.
-if test "${enable_html_doc+set}" = set; then
- enableval="$enable_html_doc"
- :
-else
- enable_html_doc=yes
-fi
-
-# Check whether --enable-ps-doc or --disable-ps-doc was given.
-if test "${enable_ps_doc+set}" = set; then
- enableval="$enable_ps_doc"
- :
-else
- enable_ps_doc=yes
-fi
-
-# Check whether --with-cint or --without-cint was given.
-if test "${with_cint+set}" = set; then
- withval="$with_cint"
- :
-else
- with_cint=no
-fi
-
-