Delete pushtomaster.sh

`dev` is dead
2019-08-20 15:17:35 +02:00
parent 648f26f075
commit 48a245559c
1 changed files with 0 additions and 4 deletions
@@ -1,4 +0,0 @@
-git checkout master
-git merge --ff-only dev
-git push origin master
-git checkout dev