Merging now to prevent conflict with #8614.

PS This adds an annoying extra 1:30 or so to the end of the build on the master branch, rather than nicely running in parallel.

The docs_and_coverage step ran coverage on one node, all the rest on the other. But now the docs and translations have to wait for the coverage to finish.

The issue with the context suffered by @hius07, @zwim and others should be resolved by ec280f8.

Seems it isn't with #8616 :/

My usual web UI workflow in my repository to make a PR:
-fetch upstream of koreader:master
-create a branch
-commit changes to the branch
-compare and make a PR to koreader:master
CircleCI doesn't start.
After merging the PR to koreader:master CircleCI starts.
Maybe I need some settings in the repository? My Actions page shows only macos_build:
https://github.com/hius07/koreader/blob/master/.github/workflows/build.yml
There is no CircleCI there.

https://support.circleci.com/hc/en-us/articles/360008097173-Why-aren-t-pull-requests-triggering-jobs-on-my-organization-

Sometimes you'll have a user who submits a pull request to your repository from a fork, but no pipeline will be triggered with the pull request. This can happen when the user is following the project fork on their personal account rather than the project itself on CircleCI.

This will cause the jobs to trigger under the user's personal account. If the user is following a fork of the repository on CircleCI, we will only build on that fork and not the parent, so the parent’s PR will not get status updates.

In these cases have the user unfollow their fork of the project on CircleCI and follow the source project instead. This will trigger their jobs to run under the organization when they submit pull requests.

Great! Thanks a lot!

It worked? Neat! :-)