diff --git a/build b/build
index 2d98e862..b209e1c2 100755
--- a/build
+++ b/build
@@ -130,6 +130,7 @@ case "$1" in
       git push --mirror
       git push --mirror github
       git push --mirror sf
+      git push --mirror ethz
    ;;
 
    clean)