diff --git a/build b/build index 69f0ad92..9e9fbf21 100755 --- a/build +++ b/build @@ -114,6 +114,7 @@ case "$1" in p|pu|pub) git push --mirror git push --mirror github + git push --mirror sf ;; clean)