Add tag push to release process

1 files changed, 3 insertions, 0 deletions

diff --git a/RELEASE b/RELEASE
index c1b0568..7100898 100644
--- a/RELEASE
+++ b/RELEASE
@@ -10,6 +10,9 @@ commit release changes
 create a tag
     git tag -s $VERSION
 
+push the tag
+    git push --tags
+
 archive's creation :
     git archive --format=tar.gz --prefix=mat-$VERSION/ $VERSION > mat-$VERSION.tar.gz