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

Add linter.deprecated option to silence deprecation warnings #1768

Merged
merged 1 commit into from
Oct 23, 2022

Conversation

digama0
Copy link
Collaborator

@digama0 digama0 commented Oct 22, 2022

Although the deprecation warning is not, strictly speaking, a linter, it makes sense from a user standpoint to treat it as one. This adds a linter.deprecated option you can turn off in order to silence / acknowledge deprecation warnings. The Lean.Linter.Util file had to be split up to give access to the linter option access function.

@Kha Kha changed the title feat: add linter.deprecated option to silence deprecation warnings Add linter.deprecated option to silence deprecation warnings Oct 22, 2022
@Kha Kha added the changelog label Oct 22, 2022
@Kha Kha merged commit c4cbefc into leanprover:master Oct 23, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants