fix rebase

kim-em · kim-em · commit ef2b965eac95 · 2025-11-04T00:38:26.000+01:00
diff --git a/lakefile.lean b/lakefile.lean
@@ -34,6 +34,7 @@ abbrev mathlibOnlyLinters : Array LeanOption := #[
   ⟨`linter.tacticAnalysis.tryAtEachStepAesop, true⟩,
   ⟨`linter.tacticAnalysis.tryAtEachStepSimpAll, true⟩,
   ⟨`linter.tacticAnalysis.tryAtEachStepGrind, true⟩,
+  ⟨`linter.tacticAnalysis.tryAtEachStepGrindSuggestions, true⟩,
   -- ⟨`linter.nightlyRegressionSet, true⟩,
   -- `latest_import.yml` uses this comment: if you edit it, make sure that the workflow still works
 ]

Original file line number	Diff line number	Diff line change
`@@ -34,6 +34,7 @@ abbrev mathlibOnlyLinters : Array LeanOption := #[`
`34`	`34`	⟨`linter.tacticAnalysis.tryAtEachStepAesop, true⟩,
`35`	`35`	⟨`linter.tacticAnalysis.tryAtEachStepSimpAll, true⟩,
`36`	`36`	⟨`linter.tacticAnalysis.tryAtEachStepGrind, true⟩,
	`37`	+ ⟨`linter.tacticAnalysis.tryAtEachStepGrindSuggestions, true⟩,
`37`	`38`	-- ⟨`linter.nightlyRegressionSet, true⟩,
`38`	`39`	-- `latest_import.yml` uses this comment: if you edit it, make sure that the workflow still works
`39`	`40`	`]`