Commit 2024-05-24 03:47 f966474a
View on Github →feat: syntax linter for #-commands (#11019)
A Lean-linter implementation of the #-command linter introduced in #10809.
This linter produces a warning whenever a non-allowed #-command is used. The allowed commands are
#align
#align_import
#noalign
#adaptation_note