Commit 2024-08-15 23:53 7a3e6979

feat: remove lint-style.sh (#15051) In detail, this PR

• moves the executable bit check into the .yml files, instead of the shell script
• adds a --fix flag to lint-style, for fixing style errors (when possible)
• moves calling lint-style.py into lake exe lint-style, and
• switches the CI workflow to call lake exe lint-style instead, and removes lint-style.sh Ideally, lint-style.py will be completely rewritten in Lean soon, so this calling of an external process is only temporary. Helps with #14539.