mathlib
fe69dea0 - chore(gitpod): be slightly more intelligent about getting a PR cache

Commit

4 years ago

chore(gitpod): be slightly more intelligent about getting a PR cache Having any cache is much better than starting up gitpod and having no cache at all.

References

eric-wieser/gitpod-cache

Author

eric-wieser

Parents

b681b6b9

mathlib fe69dea0 - chore(gitpod): be slightly more intelligent about getting a PR cache

mathlib
fe69dea0 - chore(gitpod): be slightly more intelligent about getting a PR cache