diff options
| author | Alan Wu <XrXr@users.noreply.github.com> | 2021-07-26 20:19:01 -0400 |
|---|---|---|
| committer | Alan Wu <XrXr@users.noreply.github.com> | 2021-10-20 18:19:38 -0400 |
| commit | 5b4305f71c90d498c91d7b5038758e3557938802 (patch) | |
| tree | c4e8212eafd53a10e85f8d54a770e94fa3c7c88b /include | |
| parent | 8cf01dd25c126cf19b9146b71992b53c4541382e (diff) | |
Simpler fix for -DUSE_EMBED_CI=0
Nobu pointed out that saving the old ci to a local is enough to keep it
reachable.
Diffstat (limited to 'include')
0 files changed, 0 insertions, 0 deletions