diff options
| -rwxr-xr-x | configure | 9 |
1 files changed, 5 insertions, 4 deletions
@@ -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 ########################################## |