diff options
| -rw-r--r-- | doc/STYLE_GUIDE.md | 4 | ||||
| -rw-r--r-- | doc/onboarding.md | 3 |
2 files changed, 4 insertions, 3 deletions
diff --git a/doc/STYLE_GUIDE.md b/doc/STYLE_GUIDE.md index d1bf520859..8ea9c8fe81 100644 --- a/doc/STYLE_GUIDE.md +++ b/doc/STYLE_GUIDE.md @@ -9,9 +9,7 @@ * The formatting described in `.editorconfig` is preferred. * A [plugin][] is available for some editors to automatically apply these rules. -* Mechanical issues, like spelling and grammar, should be identified by tools, - insofar as is possible. If not caught by a tool, they should be pointed out by - human reviewers. +* Changes to documentation should be checked with `make lint-md`. * American English spelling is preferred. "Capitalize" vs. "Capitalise", "color" vs. "colour", etc. * Use [serial commas][]. diff --git a/doc/onboarding.md b/doc/onboarding.md index 1491b5ee9e..e67f6638d3 100644 --- a/doc/onboarding.md +++ b/doc/onboarding.md @@ -121,6 +121,9 @@ onboarding session. avoid stalling the pull request. * Note that they are nits when you comment: `Nit: change foo() to bar().` * If they are stalling the pull request, fix them yourself on merge. +* Insofar as possible, issues should be identified by tools rather than human + reviewers. If you are leaving comments about issues that could be identified + by tools but are not, consider implementing the necessary tooling. * Minimum wait for comments time * There is a minimum waiting time which we try to respect for non-trivial changes, so that people who may have important input in such a distributed |