[metrics-bugs] #25275 [Internal Services/Service - git]: Please delete tag collector-1.5.0 in collector.git

[Tor Bug Tracker & Wiki]

#25275: Please delete tag collector-1.5.0 in collector.git
-------------------------------------------------+------------------------
     Reporter:  karsten                          |      Owner:  tor-gitadm
         Type:  task                             |     Status:  new
     Priority:  Medium                           |  Milestone:
    Component:  Internal Services/Service - git  |    Version:
     Severity:  Normal                           |   Keywords:
Actual Points:                                   |  Parent ID:
       Points:                                   |   Reviewer:
      Sponsor:                                   |
-------------------------------------------------+------------------------
 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!

--
Ticket URL: <https://trac.torproject.org/projects/tor/ticket/25275>
Tor Bug Tracker & Wiki <https://trac.torproject.org/>
The Tor Project: anonymity online