bin/git-update.sh: Also push tags to remotes.

diff --git a/bin/git-update.sh b/bin/git-update.sh
index 83080b965dfb42fb2a689bbc375537fb3ade1101..e9c0abad5b79e4e983d862b58e0fdd29b493f7e2 100755 (executable)
--- a/bin/git-update.sh
+++ b/bin/git-update.sh
@@ -18,6 +18,7 @@ git remote update 2>&1 | grep -v Fetching
 # Push all local changes to remote(s).
 for remote in `git remote`; do
     git push $remote 2>&1 | grep -v 'Everything up-to-date'
+    git push --tags $remote 2>&1 | grep -v 'Everything up-to-date'
 done
 # Show unmerged changes.
 git branch -rv --color --no-merged