do not push to ethz

Signed-off-by: Nico Schottelius <nico@brief.schottelius.org>
12 years ago · acb31b2632
parent fbda50dfb0
commit acb31b2632
1 changed files with 1 additions and 1 deletions
--- a/2
+++ b/2
@ -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