From fada3e872a81d97a6f7879ae26d13d6be17a9f2a Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 14 Oct 2024 12:17:43 +0000
Subject: [PATCH] chore: no need to suppress Aesop warning (#17716)

---
 lakefile.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/lakefile.lean b/lakefile.lean
index a4a09667f6c2b..59b2eae8ed37f 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -35,8 +35,7 @@ abbrev mathlibOnlyLinters : Array LeanOption := #[
   ⟨`linter.style.longLine, true⟩,
   ⟨`linter.style.longFile, .ofNat 1500⟩,
   ⟨`linter.style.missingEnd, true⟩,
-  ⟨`linter.style.setOption, true⟩,
-  ⟨`aesop.warn.applyIff, false⟩ -- This became a problem after https://github.com/leanprover-community/aesop/commit/29cf094e84ae9852f0011b47b6ddc684ffe4be5f
+  ⟨`linter.style.setOption, true⟩
 ]
 
 /-- These options are passed as `leanOptions` to building mathlib, as well as the