Simplify linting output in workflow

2023-08-31 10:15:12 +02:00
parent 2e0474dc71
commit 5bbb7bdd09
6 changed files with 49 additions and 35 deletions
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -669,6 +669,8 @@ Options:
  --help                          Show this message and exit.
 ```

+As a convenience, we provide a script that runs the same set of checks as our GitHub workflow. Before submitting a PR, run `tools/lint.sh` and fix any errors. You can use the tools described above to find out more about the failures.
+
 The test workflow runs test suites in parallel. Refer to the next section for more details on running and writing tests.

 ## Using and writing tests