From 9428537fd4610afaae3d1bf535ef0a7ee11fa5f7 Mon Sep 17 00:00:00 2001
From: Rusty Russell <rusty@rustcorp.com.au>
Date: Wed, 23 Nov 2011 13:06:00 +1030
Subject: [PATCH] Makefile-web: push to github repo too.

Saves me doing it manually.
---
 Makefile-web | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Makefile-web b/Makefile-web
index d6ea6cc9..10671edc 100644
--- 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 .
-- 
2.39.2