Tim Ruffing 9361f360bb ci: Select number of parallel make jobs depending on CI environment ...

This should improve compilation times on macOS. Things can certainly
be improved further, e.g., by running the benchmarks in parallel.

2021-03-03 18:16:25 +01:00

..

cirrus.sh

ci: Select number of parallel make jobs depending on CI environment

2021-03-03 18:16:25 +01:00

linux-debian.Dockerfile

ci: Run PRs on merge result instead of on the source branch

2021-03-03 01:21:11 +01:00