Meta/pushall: publish HTML docs to GitHub Pages, too

diff --git a/pushall b/pushall
index 4f7a904536491fd09a7dccb0a1249f938b30b54b..782680d2299a52afe82c1d8d7d6e68fec0a9447a 100755 (executable)
--- a/pushall
+++ b/pushall
@@ -45,5 +45,6 @@ case "$#,$*" in
                printf "%s: " "$topic"
                ( cd ../git-$topic.git && git push "$@") || exit
        done
+       test "$1" = '-n' || ( cd ../git-htmldocs.git && git push gh-pages )
        ;;
 esac