maint/push-to-public: Push including tags

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