No need to do this in as many jobs. Splitting all the github stuff from
docker stuff into two jobs is enough. This still allows to conditionally
enable docker jobs in contributors repos, depending on whether the
relevant docker credentials are provided - but avoids using too many
concurrent runners.
Wolfgang Walther
9d67febb93