Meta/pushall: adjust to new layout

diff --git a/pushall b/pushall
index 7755a181ed54f1ad832257ab395f25f5dfe99390..872818d12d0d24ac7949ef49120ad6ca264bf56c 100755 (executable)
--- a/pushall
+++ b/pushall
@@ -9,7 +9,11 @@ done
 case "$#" in
 0)
        printf "github mirror: "
-       git push github "$@" ;;
-*)
-       echo "No push to github" ;;
+       git push github "$@" || exit $?
+       for topic in htmldocs manpages
+       do
+               printf "%s: " "$topic"
+               ( cd ../git-$topic.git && git push ) || exit
+       done
+       ;;
 esac