From acb31b2632778e1dc2eaf32fbf9d2bc5cf8d4da6 Mon Sep 17 00:00:00 2001
From: Nico Schottelius <nico@brief.schottelius.org>
Date: Wed, 19 Dec 2012 22:41:20 +0100
Subject: [PATCH] do not push to ethz

Signed-off-by: Nico Schottelius <nico@brief.schottelius.org>
---
 build | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/build b/build
index 572fb768..1f408b94 100755
--- a/build
+++ b/build
@@ -349,7 +349,7 @@ eof
     ;;
 
      p|pu|pub)
-          for remote in "" github sf ethz; do
+          for remote in "" github sf; do
                 echo "Pushing to $remote"
                 git push --mirror $remote
           done