Commit 2024-06-25 01:47 55f62404
View on Github →feat: rewrite line length style linter in Lean (#14093) And finish moving the broad imports linter to Lean: I forgot to remove the Python code and actually run the Lean code, oops.
feat: rewrite line length style linter in Lean (#14093) And finish moving the broad imports linter to Lean: I forgot to remove the Python code and actually run the Lean code, oops.