From d68c2ce28bc11ec0271a97aa7a7316905f15a484 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 2 Feb 2025 09:54:57 +0100 Subject: [PATCH] chore: remove stray profiler option from test --- tests/lean/run/grind_constProp.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/tests/lean/run/grind_constProp.lean b/tests/lean/run/grind_constProp.lean index acd43b7a66..692e805a8c 100644 --- a/tests/lean/run/grind_constProp.lean +++ b/tests/lean/run/grind_constProp.lean @@ -5,8 +5,6 @@ set_option grind.warning false attribute [grind cases] Or attribute [grind =] List.length_nil List.length_cons Option.getD -set_option profiler true - abbrev Var := String inductive Val where