diff options
author | hartmut@mysql.com <> | 2004-09-26 15:27:13 +0200 |
---|---|---|
committer | hartmut@mysql.com <> | 2004-09-26 15:27:13 +0200 |
commit | 5c8eb7066762fc4a864f9690f839933186ef54d5 (patch) | |
tree | 4314a45554c534ee02f77e25182f434aed118c9d /configure.in | |
parent | 42b063c3b47a784c2286a0c840b9158e8fa3e85f (diff) | |
download | mariadb-git-5c8eb7066762fc4a864f9690f839933186ef54d5.tar.gz |
added --without-man option similar to --without-docs
(part of BUG#5379)
Diffstat (limited to 'configure.in')
-rw-r--r-- | configure.in | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/configure.in b/configure.in index c3978ff32d1..37b0432b98d 100644 --- a/configure.in +++ b/configure.in @@ -2181,6 +2181,21 @@ else fi AC_SUBST(docs_dirs) +# Shall we build the man pages? +AC_ARG_WITH(man, + [ --without-man Skip building of the man pages.], + [with_man=$withval], + [with_man=yes] +) + +if test "$with_man" = "yes" +then + man_dirs="man" +else + man_dirs="" +fi +AC_SUBST(man_dirs) + # Shall we build the bench code? AC_ARG_WITH(bench, [ --without-bench Skip building of the benchmark suite.], |