Skip to content

feat: add hint to deprecated linter - #14705

Draft
wkrozowski wants to merge 7 commits into
leanprover:masterfrom
wkrozowski:wkr/deprecated-hint2
Draft

feat: add hint to deprecated linter#14705
wkrozowski wants to merge 7 commits into
leanprover:masterfrom
wkrozowski:wkr/deprecated-hint2

Conversation

@wkrozowski

Copy link
Copy Markdown
Contributor

This PR adds a clickable hint (and thus also a code action) to deprecated linter. Stacked on top of #14600.

@wkrozowski wkrozowski added the changelog-language Language features and metaprograms label Aug 6, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-language Language features and metaprograms

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants