Delete the ticket26223 branch in git.torproject.org/tor.git
Hi nickm,
It looks like you accidentally pushed ticket26223 to the canonical tor.git: https://gitweb.torproject.org/tor.git/log/?h=ticket26223
We should check if it disappears from github once it's deleted. If not, I can delete it there.