1 files changed, 7 insertions, 0 deletions

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