diff options
| author | Christian Marangi <ansuelsmth@gmail.com> | 2023-05-28 02:55:26 +0200 |
|---|---|---|
| committer | Christian Marangi <ansuelsmth@gmail.com> | 2023-05-31 13:22:03 +0200 |
| commit | 203cc0a7ef0bbf3b5a19db3caa96e91963ec154c (patch) | |
| tree | 3ad84299726636be1d3fb524b35b769578968152 /config/Config-build.in | |
| parent | 6321361c6b13a37b0cfa279a51a0cf8239a7852c (diff) | |
CI: build: add job to remove previous ccache cache if already exist
Github Actions cache doesn't permit to overwrite cache if it does
already exist. As a trick to refresh and have fresh ccache pool,
delete the ccache cache if it does exist with the help of Github REST
API. An additional permission is needed to access this API. Add this
permittion to each user of the build workflow.
Signed-off-by: Christian Marangi <ansuelsmth@gmail.com>
Diffstat (limited to 'config/Config-build.in')
0 files changed, 0 insertions, 0 deletions