tagme: Do not use git push --tags
It's dangerous, as it will push all local tags. Getting rid off unwanted
tags on the remote is not the best type of work to start your day...
Use git push origin <tag_name> instead, which will only push the
As has happened in kdevelop.git
Reviewers: O2 releaseme, sitter, bcooksley
Reviewed By: O2 releaseme, sitter
Differential Revision: https://phabricator.kde.org/D19578