diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 31cf38679..c81c0d4db 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -77,8 +77,10 @@ processed incorrectly by a type checker. It is also helpful to add links to online documentation or to the implementation of the code you are changing. -Also, do not squash your commits after you have submitted a pull request, as this +Also, do not squash your commits or use `git commit --amend` after you have submitted a pull request, as this erases context during review. We will squash commits when the pull request is merged. +This way, your pull request will appear as a single commit in our git history, even +if it consisted of several smaller commits. At present the maintainers are (alphabetically): * David Fisher (@ddfisher)