Commit 2024-09-11 09:59 53d5e938

View on Github →

fix: make print-style-errors.sh robust against file names with quotes (#16699) Notably, any file after Mathlib/Tactic/LinearCombination'.lean in the find output was not linted.

Estimated changes