Push the created tag...

diff --git a/tools/makesrcdist b/tools/makesrcdist
index b6e6c868d97a87f9c41cafb729ecea930030f8b3..7c095326ba4279c93693e5aef57c2ad2cebfd165 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'`