[tor-bugs] #18088 [Service - git]: Please delete erroneously pushed branch from onionoo.git

[Tor Bug Tracker & Wiki]

#18088: Please delete erroneously pushed branch from onionoo.git
-------------------------------+------------------------
     Reporter:  karsten        |      Owner:  tor-gitadm
         Type:  task           |     Status:  new
     Priority:  Medium         |  Milestone:
    Component:  Service - git  |    Version:
     Severity:  Normal         |   Keywords:
Actual Points:                 |  Parent ID:
       Points:                 |    Sponsor:
-------------------------------+------------------------
 Branch task-16907-2 should have been pushed to my public repository, but
 instead I pushed it to the official repository.  Now I cannot delete it
 anymore:

 {{{
 ~/src/onionoo$ git push origin --delete task-16907-2
 remote: + refs/heads/task-16907-2 onionoo karsten DENIED by fallthru
 remote: error: hook declined to update refs/heads/task-16907-2
 To ssh://git@git-rw.torproject.org/onionoo.git
  ! [remote rejected] task-16907-2 (hook declined)
 error: failed to push some refs to 'ssh://git@git-
 rw.torproject.org/onionoo.git'
 }}}

 Thanks in advance!

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