Commit 2024-06-24 11:40 df87079f

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.