# HG changeset patch
# User diego
# Date 1280311256 0
# Node ID d55bcadba17a21fe63f88074bd7dc506919de848
# Parent  6f79e6b02ed861d3f7f4aadc24e647269ebf8a26
Skip searching for an xmllint command.
The xmllint target is separate from building the documentation; thus if xmllint
is not available, the xmllint targets can fail without further harm.

diff -r 6f79e6b02ed8 -r d55bcadba17a DOCS/xml/configure
--- a/DOCS/xml/configure	Wed Jul 28 09:53:01 2010 +0000
+++ b/DOCS/xml/configure	Wed Jul 28 10:00:56 2010 +0000
@@ -177,17 +177,8 @@
 fi
 
 
-echo "Searching for XML checker..."
-if command -v xmllint > /dev/null 2>&1; then
-  echo "Found xmllint"
-  xmllint_command="xmllint --noout --noent --postvalid $catalog_opts \$*"
-else
-  echo "Not found"
-  xmllint_command=true
-fi
-
 cat > xml.mak << EOF
 CATALOG = $catalog
-XMLLINT_COMMAND = $xmllint_command
+XMLLINT_COMMAND = xmllint --noout --noent --postvalid $catalog_opts \$*
 XSLT_COMMAND = $xsltcommand
 EOF