diff --git a/tools/push b/tools/push new file mode 100755 index 00000000..7b149e8f --- /dev/null +++ b/tools/push @@ -0,0 +1,7 @@ +#!/bin/sh + +git checkout master +git merge --no-ff next +git checkout next +git rebase master +git push