Mario Carneiro (Mar 23 2021 at 02:09):
Currently, if the latest commit of a PR is in progress,
leanproject up becomes somewhat self-defeating, because it always pulls to get the latest version even if that commit doesn't have a cache. Would it be possible to modify the behavior so that it gets the last version that has a cache? It should also set the remaining files as dirty so that lean knows to compile them, if necessary (I think this is automatic).
Bryan Gin-ge Chen (Mar 23 2021 at 02:38):
This was also suggested here. (I haven't had time to work on this.)
Last updated: Aug 03 2023 at 10:10 UTC