From e392792e1e5dc25b5e9ad49621b0c29e33fabc32 Mon Sep 17 00:00:00 2001
From: Nico Schottelius <nico@kr.ethz.ch>
Date: Sat, 20 Aug 2011 23:31:52 +0200
Subject: [PATCH] also push to github by default

Signed-off-by: Nico Schottelius <nico@kr.ethz.ch>
---
 Makefile | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index f2867d7..f44a849 100644
--- a/Makefile
+++ b/Makefile
@@ -174,7 +174,8 @@ t2:
 # Developer targets
 #
 pub:
-	@git push
+	git push
+	git push github
 
 publish-doc: documentation
 	@echo "Transferring files to ${host}"