Remove branches from origin that have been merged into master except devel

gistfile1.sh

git fetch
git checkout master
git branch --merged | grep -v "\*" | grep -v devel | xargs -n 1 git push --delete origin 

# this last step is for colleagues to clean up their local tracking branches
git remote prune origin