maint/push-to-public: git push --tags requires branches

diff --git a/maint/push-to-public b/maint/push-to-public
index 4ed9467e883326667b314dbd7530f16410c8039b..cb550fb1cb427eb3f8a4b1e1726f7711b089693e 100755 (executable)
--- a/maint/push-to-public
+++ b/maint/push-to-public
@@ -1,4 +1,4 @@
 #!/bin/sh
 set -e
-git push --tags public
-git push --tags github
+git push --tags public master
+git push --tags github master