diff options
| author | Théo Zimmermann | 2019-06-03 16:28:18 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-06-03 16:28:18 +0200 |
| commit | f051e10bbd357cd45d5b24b30abac325b0057b95 (patch) | |
| tree | e7ae26c331d392fb9904fd29741c467123565618 | |
| parent | 147666df9d71056e614acbab0b0b5935a085bf32 (diff) | |
| parent | 573d33f49433f7b1dce3603c8138c0ded726cfc5 (diff) | |
Merge PR #10280: Fixed typo in CONTRIBUTING.md
Reviewed-by: Zimmi48
| -rw-r--r-- | CONTRIBUTING.md | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index e811c116b6..f0e17909c1 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -169,7 +169,7 @@ People are generally happy to help and very reactive. ["Watching" this repository](https://github.com/coq/coq/subscription) can result in a very large number of notifications. We advise that if -you do, either [confifure your mailbox](https://blog.github.com/2017-07-18-managing-large-numbers-of-github-notifications/#prioritize-the-notifications-you-receive) +you do, either [configure your mailbox](https://blog.github.com/2017-07-18-managing-large-numbers-of-github-notifications/#prioritize-the-notifications-you-receive) to handle incoming notifications efficiently, or you read your notifications within a web browser. You can configure how you receive notifications in [your GitHub settings](https://github.com/settings/notifications), |