Commit 2026-10-05 16:14 c20717ea

chore(Linter): use ModuleLinter for missingEnd and privateModule (#44517) As of recently, Lean supports module linters: these are like normal syntax linters, but they only run at the end of a file, instead of at each command. This PR refactors two linters to be a ModuleLinter, because they are meant to only run at the end of the file. Previously, these linters would look at every piece of syntax, and check whether it is the end of the file. Now, they automatically only run at the end of the file. A module linter gets passed an array of all syntaxes, which these linters simply ignore. It looks like there was no test for the missingEnd linter, so I have added one. The message it outputs looks a bit weirdly formatted, but fixing this is outside the scope of this PR.