Please sign in to comment.
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...