[PATCH] configure: add --without-api-docs option

[David Bremner]

mp39590 at gmail.com writes:

> From: Mikhail <mp39590 at gmail.com>
>
> Add option to explicitly disable API man page build even if doxygen is
> available.

I'm not sure about the use case here. For some reason you want to
install some of the man pages, but not all of them?

> ---
>  configure | 14 ++++++++++++--
>  1 file changed, 12 insertions(+), 2 deletions(-)
>
> diff --git a/configure b/configure
> index ae0a027..a6b6ee8 100755
> --- a/configure
> +++ b/configure
> @@ -68,6 +68,7 @@ PYTHON=${PYTHON:-}
>  PREFIX=/usr/local
>  LIBDIR=
>  WITH_DOCS=1
> +WITH_API_DOCS=1
>  WITH_EMACS=1
>  WITH_BASH=1
>  WITH_RUBY=1
> @@ -137,7 +138,8 @@ Some features can be disabled (--with-feature=no is equivalent to
>  --without-feature) :
>  
>  	--without-bash-completion	Do not install bash completions files
> -	--without-docs			Do not install documentation and man pages
> +	--without-docs			Do not install man pages

I would say that --without-docs should imply --without-api-docs

I'm not totally convinced about the change in the description, but I
guess we can always change it back if / when we start install other
kinds of docs (e.g. html docs or info pages).