Merge branch 'master' into crem

Conflicts:
	tools/dev/push.sh

diff --cc tools/dev/push.sh
index 3b99d10b06f942ca616b715967e7708da2132a7f,bc221452addfb174911f75a5f9caa4e10b7f01a3..6a3288a5d91b2e7db7205e84d2be482fe4015baf
--- 1/tools/dev/push.sh
--- 2/tools/dev/push.sh
+++ b/tools/dev/push.sh
@@@ -4,13 -4,11 +4,8 @@@ git branch | tr -d \* | while read lin
  do
      branch=${line/#\ }
  
 -    echo "Push $branch to origin:"
      git push origin $branch
 -
 -    echo "Push $branch to github:"
      git push hub $branch
-  
- #    if [[ $branch == *master* ]]; then
- #        echo "Push $branch to github:"
- #        git push hub $branch
- #    fi
  
  done