Commit 2024-06-24 11:40 df87079f
View on Github →chore: move lint_style
executable to the scripts
directory (#14057)
Otherwise, importing Mathlib.Tactic
makes defining own executables impossible, as the main
function in Linter.TextBased
would collide with any other main function. Move the code for the lint_style executable to scripts (which arguably might be a better place anyway); we leave the text-based linters in Tactic/Linter.