Commit 2024-08-02 08:48 9c39e72d

feat: rewrite updating style-exceptions in Lean (#14697) Rewrite the update-style-exceptions script in Lean, by adding an --update flag to lint_style: in this mode, the script will remove any exceptions which are no longer needed, add new entries for any current error, and try to leave existing entries untouched. (With one exception: if a "file too long" error still applies, but the file is currently at least 200 lines shorter, we update it to the new entry.)