Skip to content

feat: add hint to deprecated linter - #14705

Merged
wkrozowski merged 1 commit into
leanprover:masterfrom
wkrozowski:wkr/deprecated-hint2
Aug 14, 2026
Merged

wkrozowski merged 1 commit into
leanprover:masterfrom
wkrozowski:wkr/deprecated-hint2

feat: add hint to `deprecated` linter

7938242
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
check-stdlib-flags
succeeded Aug 14, 2026 in 5s