release.sh: don't forget to push as well as push tags

diff --git a/re2c/release.sh b/re2c/release.sh
index bd9659eabc9b88211352dbada5bb4d96714fee1d..5b44a0878f5ccdd98db5368b646cfd6254698833 100755 (executable)
--- a/re2c/release.sh
+++ b/re2c/release.sh
@@ -42,6 +42,7 @@ rm -r $tmpdir
 # commit release
 git commit -a -m "Release $version."
 git tag $version
+git push
 git push --tags
 
 # upload files on sourceforge