From 9cef7a0d3d796007006f263f7edcbadd58dd7140 Mon Sep 17 00:00:00 2001
From: Miek Gieben <miek@miek.nl>
Date: Wed, 10 Jan 2018 08:17:22 +0000
Subject: [PATCH] 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.
---
 Makefile.release | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Makefile.release b/Makefile.release
index 4069eb08..8fb748e8 100644
--- a/Makefile.release
+++ b/Makefile.release
@@ -49,3 +49,4 @@ commit:
 push:
 	@echo Pushing release $(VERSION) to master
 	git push --tags
+	git push