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