all branches to github

diff --git a/tools/dev/push.sh b/tools/dev/push.sh
index 6369c231e924bb8b984854d145d71421e29a0a8f..bc221452addfb174911f75a5f9caa4e10b7f01a3 100755 (executable)
--- a/tools/dev/push.sh
+++ b/tools/dev/push.sh
@@ -7,10 +7,8 @@ do
     echo "Push $branch to origin:"
     git push origin $branch
 
-    if [[ $branch == *master* ]]; then
-        echo "Push $branch to github:"
-        git push hub $branch
-    fi
+    echo "Push $branch to github:"
+    git push hub $branch
 
 done