Please delete tag collector-1.5.0 in collector.git
I accidentally pushed a tag to the official CollecTor repository, and now I cannot delete it anymore:
$ git push --delete origin collector-1.5.0
remote: + refs/tags/collector-1.5.0 collector karsten DENIED by fallthru
remote: error: hook declined to update refs/tags/collector-1.5.0
To ssh://git-rw.torproject.org/collector
! [remote rejected] collector-1.5.0 (hook declined)
error: failed to push some refs to 'ssh://git@git-rw.torproject.org/collector'
Can somebody with Git superpowers please delete the collector-1.5.0 tag? Thanks in advance!