diff options
Diffstat (limited to 'maintainer-scripts/update_web_docs')
| -rwxr-xr-x | maintainer-scripts/update_web_docs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/maintainer-scripts/update_web_docs b/maintainer-scripts/update_web_docs index 6872a4a..63df12f 100755 --- a/maintainer-scripts/update_web_docs +++ b/maintainer-scripts/update_web_docs @@ -167,7 +167,7 @@ if [ "$RELEASE" = "HEAD" ]; then # Preprocess the entire web site, not just the install docs! echo "Invoking $WWWPREPROCESS" - $WWWPREPROCESS + $WWWPREPROCESS |grep -v '^ Warning: Keeping' fi # Clean up behind us. |
