Push the created tag.

diff --git a/tools/makesrcdist b/tools/makesrcdist
index 60c4a1dbcf9f98cf1f186a996cf3600acbc15fe9..bfc96093e67cdd3da4d2357127336ae3e2c82085 100755 (executable)
--- a/tools/makesrcdist
+++ b/tools/makesrcdist
@@ -77,6 +77,7 @@ else
 
        echo Creating tag for release...
        git tag -m "Tag $version" release-$version
+       git push origin release-$version
 fi
 
 fileurl=`echo $fileurl | sed -e '1,$s/\\//\\\\\\//g'`