Re: [PATCH v3 2/2] ci: use twice the CPU count on both providers

> GitHub Actions sets JOBS to ten regardless of runner size, while
> GitLab CI uses the detected CPU count. Use twice the CPU count for
> Make and prove on both providers, doubling GitLab's job count.
> 
> Five GitHub Actions attempts per policy, with the long tests enabled,
> gave these sums of per-job median successful build/test-step times
> (minutes; four or five samples per job) [1-3]:
> 
>                       Fixed 10   CPU count   2x CPU count
>   Linux Make             278.9       273.9          259.9
>   macOS Make              94.5       119.1           99.8
>   Windows Make           102.2       103.8          100.8
> 
> Workflow overhead is excluded; Windows runner images varied.
> 
> Use twice the CPU count to scale concurrency with runner size while
> avoiding the larger macOS slowdown observed with one job per CPU.
> Compared with ten jobs, this trades a lower Linux total for a higher
> macOS total.