Commit 2026-04-23 20:27 8f4785ce
View on Github →feat: warn on deprecated declarations in scripts/check-yaml (#38313)
This PR updates scripts/check-yaml.lean to warn on deprecated declarations.
It also cleans up some code: initSearchPath does exactly what the removed code plus CoreM.withImportModules does (and as far as I can see we no longer need CoreM). Also modulizes and removes the dependence on Mathlib.