Documentation: explain push.default option a bit more

diff --git a/Documentation/install-webdoc.sh b/Documentation/install-webdoc.sh
index 37e67d1a14aa6f8ef5c8914054c03cc6f5cc762b..76d69a907b48a961906e0b85c59a75e9c0c8986d 100755 (executable)
--- a/Documentation/install-webdoc.sh
+++ b/Documentation/install-webdoc.sh
@@ -6,7 +6,7 @@ for h in \
        *.txt *.html \
        howto/*.txt howto/*.html \
        technical/*.txt technical/*.html \
-       RelNotes-*.txt *.css
+       RelNotes/*.txt *.css
 do
        if test ! -f "$h"
        then
@@ -30,7 +30,7 @@ for th in \
 do
        h=`expr "$th" : "$strip_leading"'\(.*\)'`
        case "$h" in
-       index.html) continue ;;
+       RelNotes-*.txt | index.html) continue ;;
        esac
        test -f "$h" && continue
        echo >&2 "# rm -f $th"