Deleting git tags?

[Carlos O'Donell <carlos at systemhalted dot org>]

Community,

Last night I created several tags in both the core
and ports repos to mark the commits at which the
libc.pot file was sent to the translation project.

Since then we've talked about what to call these
tags to avoid confusion.

Given that I haven't uploaded a 2.15.1 snapshot
for the translation team I decided I would delete
these tags and follow the new naming convention.

I've delted the glibc-2.15.1-tps tag from the ports
repsoitory with no problem.

However, deleting the remote branch on the core repo
results in:

carlos@lios:~/src/glibc-2.15$ git tag -d glibc-2.15.1-tps
Deleted tag 'glibc-2.15.1-tps' (was 88f501d)
carlos@lios:~/src/glibc-2.15$ git push origin
:refs/tags/glibc-2.15.1-tps
remote: *** Deleting a tag is not allowed in this repository
remote: error: hook declined to update refs/tags/glibc-2.15.1-tps
To ssh://carlos@sourceware.org/git/glibc.git
 ! [remote rejected] glibc-2.15.1-tps (hook declined)
error: failed to push some refs to
'ssh://carlos@sourceware.org/git/glibc.git'

Are we disallowing tag deletion because it's akin to
rewriting history?

The problem I have with that is that tags are used for
logical purposes, and mistakes show up in the tag list.
Mistakes in a commit are quickly lost in the logs but
not so for tags.
 
We should be allowed to manage tags as we like to keep
the list clean.

The only other problem is that users have to manage
keeping their local tags in sync with the remote repo,
but that's a question for another day (there are scripts
for doign this).

Comments?

Cheers,
Carlos.