diff options
| author | Enrico Tassi | 2020-12-14 12:01:29 +0100 |
|---|---|---|
| committer | GitHub | 2020-12-14 12:01:29 +0100 |
| commit | 477cba2c8906c2007b6aa6c9aa2b352d096ec844 (patch) | |
| tree | 4bc3248e82f8c24faf3e34c201f1fc63847e2244 /dev/ci/ci-basic-overlay.sh | |
| parent | 8817a18edc9185891d48e0da9e214a678fb97b75 (diff) | |
Update dev/tools/pin-ci.sh
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Diffstat (limited to 'dev/ci/ci-basic-overlay.sh')
0 files changed, 0 insertions, 0 deletions