Makefile-web: push to github repo too.
authorRusty Russell <rusty@rustcorp.com.au>
Wed, 23 Nov 2011 02:36:00 +0000 (13:06 +1030)
committerRusty Russell <rusty@rustcorp.com.au>
Wed, 23 Nov 2011 02:36:00 +0000 (13:06 +1030)
Saves me doing it manually.

Makefile-web

index d6ea6cc94806857bbee651ec15c735988a093128..10671edc74efa7aa66c806ce25bbe4e4565655bc 100644 (file)
@@ -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 .