Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
Branches sometimes don't get deleted #525
We're getting occasional crashes when Bors tries to delete a merged branch:
This was for Microsoft/openenclave#826
The branch had to be manually deleted instead.