diff --git a/configure b/configure index b2a254024144704905e32c9ba82b5f9834af2bd2..d3788fcc15b630c05b627a8452b2046d9db261a2 100755 --- a/configure +++ b/configure @@ -177,7 +177,7 @@ softmmu="yes" linux_user="no" darwin_user="no" bsd_user="no" -build_docs="no" +build_docs="yes" uname_release="" curses="yes" pthread="yes" @@ -492,6 +492,8 @@ for opt do ;; --with-pkgversion=*) pkgversion=" ($optarg)" ;; + --disable-docs) build_docs="no" + ;; *) echo "ERROR: unknown option $opt"; show_help="yes" ;; esac @@ -1236,9 +1238,8 @@ EOF fi # Check if tools are available to build documentation. -if [ -x "`which texi2html 2>/dev/null`" ] && \ - [ -x "`which pod2man 2>/dev/null`" ]; then - build_docs="yes" +if test "$build_docs" = "yes" -a \( ! -x "`which texi2html 2>/dev/null`" -o ! -x "`which pod2man 2>/dev/null`" \) ; then + build_docs="no" fi ##########################################