ci: Describe running locally

Doing so gives the developer feedback early on, before the changes hit
the GitHub CI infrastructure.

This would be a good candidate for using a Git pre-hook. Unfortunately,
gitlint is a bit tricky to be used in a pre-push hook:
jorisroovers/gitlint#55

README.md

@@ -77,6 +77,8 @@ To check if your code matches the expected style, the following commands are hel
 If existing code gets reformatted, this must be done in a separate commit. Its commit id has to be added to the file
 `.git-blame-ignore-revs` and committed in yet another commit!.
 
+### Running CI tests locally
+To avoid unneeded load on the GitHub infrastructure, please consider running `tools/ci/run_ci.sh --all` before pushing.
 
 ## Examples