diff options
| author | Rémi Verschelde <rverschelde@gmail.com> | 2022-01-11 20:59:06 +0100 |
|---|---|---|
| committer | Rémi Verschelde <rverschelde@gmail.com> | 2022-01-11 20:59:06 +0100 |
| commit | 56838ca009ca7d20eb89e7b1c182beff1ce1190d (patch) | |
| tree | 4062170d7182c3b04ffc1840c3763d52f15592ab /doc/tools | |
| parent | b6bdbd2650f48a1c98040317a857786680a6f203 (diff) | |
CI: Rename macOS cache key to force a rebuild
The cache got corrupted and until https://github.com/actions/cache/issues/2
is prioritized we're forced to fix it up with such hacks...
Diffstat (limited to 'doc/tools')
0 files changed, 0 insertions, 0 deletions