diff options
| author | Dario Nieuwenhuis <[email protected]> | 2023-07-06 02:32:49 +0200 |
|---|---|---|
| committer | Dario Nieuwenhuis <[email protected]> | 2023-07-06 02:32:49 +0200 |
| commit | 47305c2bf24c05b4956d9491478dfa53df09c47f (patch) | |
| tree | 96efcd6b1d52a6d12dbf36ee9cb8aaf801959ccf /.github/workflows | |
| parent | c421b7f5f0616e113c88d3e241de445f1e714f09 (diff) | |
ci: build doc with 4 threads instead of 6, to avoid running out of disk space.
Diffstat (limited to '.github/workflows')
0 files changed, 0 insertions, 0 deletions