Documentation: explain push.default option a bit more

diff --git a/Documentation/install-webdoc.sh b/Documentation/install-webdoc.sh
index e5c1cbea0cddac92067ab483ac4c93e3fd576c1a..76d69a907b48a961906e0b85c59a75e9c0c8986d 100755 (executable)
--- a/Documentation/install-webdoc.sh
+++ b/Documentation/install-webdoc.sh
@@ -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"