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.
miekg · Jan 10, 2018 · 9cef7a0 · 9cef7a0
1 parent 5ec25f2
commit 9cef7a0
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Makefile.release b/Makefile.release
@@ -49,3 +49,4 @@ commit:
 push:
 	@echo Pushing release $(VERSION) to master
 	git push --tags
+	git push