Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Docs: suggest deleting branches after merging PRs (#9449)
This updates the maintainer guide to recommend deleting the git branch after merging a PR. (It seems like we usually already do this, but I think we should document it to make the recommendation more official.)
- Loading branch information