diff options
| author |  Sebastiaan Zeeff <[email protected]> | 2020-11-18 23:43:57 +0100 |
|---|---|---|
| committer | Sebastiaan Zeeff <[email protected]> | 2020-11-18 23:43:57 +0100 |
| commit | 4f11ec428a5c4862598f11b8a92a65b7d13987ce (patch) | |
| tree | 75db4880cd8e42dcaeb278bcbef2656103e0f93f /scripts/dev.sh | |
| parent | Rectify production branch and clean up formatting (diff) | |
Use repository caching for master build
One problem that our master builds may have is that they retain more and
more layers of old builds, as there is no easy way of purging them from
the cache. As such master cache would not have benefits over using
repository-based caching, I've removed persistent local caching for
non-PR builds.
Diffstat (limited to 'scripts/dev.sh')
0 files changed, 0 insertions, 0 deletions