From 9e4b3d23256563319e7113280639ae61e5095d2b Mon Sep 17 00:00:00 2001 From: Nico Schottelius Date: Fri, 17 Feb 2012 10:27:23 +0100 Subject: [PATCH] +mirror Signed-off-by: Nico Schottelius --- build | 1 + 1 file changed, 1 insertion(+) 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)