[PATCH] install-webdoc: quell diff output on stdout

When installing html-doc, install-webdoc.sh compares the installed html
with the version to be installed using diff. Currently, the diff output
fills up stdout.

Redirect this to /dev/null so that the actual progress report can be
spotted again. (Note that install-webdoc.sh actually uses $DIFF so that
redirecting stdout is safer than using an option which $DIFF may or may
not understand.)

Signed-off-by: Michael J Gruber <redacted>
---
 Documentation/install-webdoc.sh |    2 +-
 1 files changed, 1 insertions(+), 1 deletions(-)

diff --git a/Documentation/install-webdoc.sh b/Documentation/install-webdoc.sh
index 34d02a2..43c09d2 100755
--- a/Documentation/install-webdoc.sh
+++ b/Documentation/install-webdoc.sh

@@ -12,7 +12,7 @@ do
 	then
 		: did not match
 	elif test -f "$T/$h" &&
-	   $DIFF -u -I'Last updated [0-9][0-9]-[A-Z][a-z][a-z]-' "$T/$h" "$h"
+	   $DIFF -u -I'Last updated [0-9][0-9]-[A-Z][a-z][a-z]-' "$T/$h" "$h" >/dev/null
 	then
 		:; # up to date
 	else

-- 
1.7.2.2.540.g9d56f.dirty