summaryrefslogtreecommitdiffstats
path: root/configure
diff options
context:
space:
mode:
authorMark Wielaard <mjw@redhat.com>2009-01-07 16:44:02 +0100
committerMark Wielaard <mjw@redhat.com>2009-01-07 16:44:02 +0100
commit2d4b8ddfb72206a2e0fc4b500e54602a1f6ba189 (patch)
treee8e958085b4f10d633f08cbb9303c8546ef2f6ac /configure
parent19a0d4b6065735b884430e3c15160997606794f1 (diff)
downloadsystemtap-steved-2d4b8ddfb72206a2e0fc4b500e54602a1f6ba189.tar.gz
systemtap-steved-2d4b8ddfb72206a2e0fc4b500e54602a1f6ba189.tar.xz
systemtap-steved-2d4b8ddfb72206a2e0fc4b500e54602a1f6ba189.zip
Warn when not building docs because tools not found.
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure8
1 files changed, 6 insertions, 2 deletions
diff --git a/configure b/configure
index 72fc7319..52b7986a 100755
--- a/configure
+++ b/configure
@@ -6560,12 +6560,16 @@ $as_echo "no" >&6; }
fi
-if test "$enable_docs" == "yes"; then
- if test "x${have_latex}${have_dvips}${have_ps2pdf}${have_latex2html}" != "xyesyesyesyes"; then
+if test "x${have_latex}${have_dvips}${have_ps2pdf}${have_latex2html}" != "xyesyesyesyes"; then
+ if test "$enable_docs" == "yes"; then
{ { $as_echo "$as_me:$LINENO: error: cannot find all tools for building documentation" >&5
$as_echo "$as_me: error: cannot find all tools for building documentation" >&2;}
{ (exit 1); exit 1; }; }
fi
+ if test "$enable_docs" == "check"; then
+ { $as_echo "$as_me:$LINENO: WARNING: will not build documentation, cannot find all tools" >&5
+$as_echo "$as_me: WARNING: will not build documentation, cannot find all tools" >&2;}
+ fi
fi
if test "x${have_latex}${have_dvips}${have_ps2pdf}${have_latex2html}" == "xyesyesyesyes" -a "$enable_docs" != "no"; then
BUILD_DOCS_TRUE=