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!
issue