Closed elhaddadyacine closed 5 years ago
You can delete the cache in Travis when you have such a problem. There is a button for that in the interface, this happens from time to time (I'm not exactly sure why). When the cache is deleted you can then restart the CI.
Thank you @rlepigre. I didn't know about such a feature in the GUI.
Hello, While trying to fix #171, Travis didn't succeed in the Deducteam/lambdapi repository but it worked with my repository elhaddadyacine/lambdapi which is very weird, I fixed the problem by deleting menhir from the installation script and put it back in the next commit which allows Travis to store a new version in the cache. I am afraid that the problem will occur for future pull requests. Is there a way to tell Travis to not get a specific package from the cache?