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