Commit 2024-07-11 14:59 1c61ab78

View on Github →

feat: add endOf linter (#14378) This linter emits a warning at the end of a file if there are unclosed namespaces or sections. All missing ends have been added (automatically) in #14621. Unlike #14352, this PR does leaves outermost noncomputable sections open. Zulip thread

Estimated changes