merge shortcut

Signed-off-by: Jeff Carr <jcarr@wit.com>
2019-06-01 15:43:08 -07:00 · 2019-06-01 15:43:08 -07:00 · 418b520835
parent 8812c70e17
commit 418b520835
1 changed files with 7 additions and 0 deletions
--- a/7
+++ b/7
@ -69,3 +69,10 @@ build-windows:
 # git push --set-upstream origin devel
 devel:
 	git checkout devel
 merge-devel:
 	git checkout master
 	git pull origin master
 	git merge devel
 	git push origin master
 	git checkout devel