Release: plain push is also needed

Apparently a git push --tags doesn't push all the changes!?! Adding plain "git push" to avoid release confusion.
2018-01-10 08:17:22 +00:00 · 2018-01-10 08:17:22 +00:00 · 9cef7a0d3d
parent 5ec25f2a50
commit 9cef7a0d3d
1 changed files with 1 additions and 0 deletions
--- a/Makefile.release
+++ b/Makefile.release
@ -49,3 +49,4 @@ commit:
 push:
 	@echo Pushing release $(VERSION) to master
 	git push --tags
+	git push