diff options
author | unknown <hartmut@mysql.com> | 2004-09-26 15:27:13 +0200 |
---|---|---|
committer | unknown <hartmut@mysql.com> | 2004-09-26 15:27:13 +0200 |
commit | 85d98034b4979b270154af305d1cb3c5f929fb0f (patch) | |
tree | 4314a45554c534ee02f77e25182f434aed118c9d /configure.in | |
parent | dc955863df5872ab4a70adbbf98d4f10d90a1f42 (diff) | |
download | mariadb-git-85d98034b4979b270154af305d1cb3c5f929fb0f.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.], |