Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

lake configuration option to suppress warning about out of date manifests? #2527

Closed
semorrison opened this issue Sep 9, 2023 · 1 comment
Assignees
Labels
enhancement New feature or request Lake Lake related issue

Comments

@semorrison
Copy link
Collaborator

Advising mathlib users to run lake update because their manifest is out of date seems to be a recipe for confused users!

Can we allow a configuration setting that suppresses this warning entirely except for particular users who "opt-in" (opting in would have to be done via some not-checked-in-to-git configuration option)?

@tydeu tydeu added enhancement New feature or request Lake Lake related issue labels Sep 10, 2023
@semorrison
Copy link
Collaborator Author

On further reflection I am less keen on this approach. Better will be to have CI ensure that users never see this warning except because of their own actions, and separately to build some guard rails around lake update.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request Lake Lake related issue
Projects
None yet
Development

No branches or pull requests

2 participants