Delete pushtomaster.sh

`dev` is dead
2019-08-20 15:17:35 +02:00 · 2019-08-20 15:17:35 +02:00 · 97baad291d
commit 97baad291d
parent 260c66f511
1 changed files with 0 additions and 4 deletions
--- a/pushtomaster.sh
+++ b/pushtomaster.sh
@ -1,4 +0,0 @@
-git checkout master
-git merge --ff-only dev
-git push origin master
-git checkout dev