Re: [PATCHv2] install-webdoc: quell diff output on stdout

Michael J Gruber [off-list ref] writes:

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.

install-webdoc.sh actually uses $DIFF, and is the only user.

I think you broke "tNNNN-X.sh -v"; isn't $DIFF used in t/ scripts
everywhere?

Even if install-webdoc.sh were the sole user (which is not), please don't
do it this way.  Instead, introduce "SHOW_PATCH_WHILE_INSTALLING_WEBDOC"
or something, and run "$DIFF" with "-q" when it is not set.

Otherwise you would forbid people from using $DIFF for its intended
purpose: name a diff binary that can be used that is different from a
crappy diff your platform gives you by default.