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=