Commits on Feb 14, 2020
- This is an option that GitHub added to their web UI last year, and I started going through repos and ticking the option manually because it wasn't in the API. - Now it's in the API (https://developer.github.com/v3/repos/#edit), so let's automatically configure all the repos to delete HEAD branches when PRs are merged. This doesn't delete the branches of PRs that are _closed_. - This saves developers time and cuts down on the amount of stale, merged branches left on repos for years going forward.