Makefile-web: push to github repo too.

Saves me doing it manually.

diff --git a/Makefile-web b/Makefile-web
index d6ea6cc94806857bbee651ec15c735988a093128..10671edc74efa7aa66c806ce25bbe4e4565655bc 100644 (file)
--- a/Makefile-web
+++ b/Makefile-web
@@ -12,6 +12,7 @@ JUNKBALLS=$(JUNKDIRS:%=$(WEBDIR)/%.tar.bz2)
 
 upload: fastcheck
        git push origin HEAD:master
+       git push github HEAD:master
 
 clean-tree:
        ! git status --porcelain | grep .