Merge develop to master and push it
#!/bin/bash
set -e
COMPANY_REMOTE=plucky
git fetch $COMPANY_REMOTE
git checkout master
git reset --hard $COMPANY_REMOTE/master
git merge --no-ff $COMPANY_REMOTE/develop
git push origin master
git push $COMPANY_REMOTE master