[tor-bugs] #31479 [Internal Services/Service - git]: Please delete branch ticket31476 from tor.git repository

[Tor Bug Tracker & Wiki]

#31479: Please delete branch ticket31476 from tor.git repository
-------------------------------------------------+------------------------
     Reporter:  nickm                            |      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 this to origin.

 My pre-push hook should have stopped me, but I got too used to overriding
 it for other things, and I accidentally overrode it for this too. :/

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