#! /bin/bash
set -ex
git pull origin
git checkout master
[ "`git status|head -n1`" = "# On branch master" ]
git fetch gdb
git merge gdb/master
git push origin master
echo OK