Skip to content

Commit d49f1ed

Browse files
committed
chore: restore privateModule initialize test with linter turned on
1 parent 8568f33 commit d49f1ed

1 file changed

Lines changed: 2 additions & 0 deletions

File tree

MathlibTest/PrivateModuleLinter/initialize.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,8 @@ import Mathlib.Tactic.Linter.PrivateModule
44

55
open Lean
66

7+
set_option linter.privateModule true
8+
79
-- Should not fire, since `initialize` has effects downstream despite creating a private decl here.
810
initialize pure ()
911

0 commit comments

Comments
 (0)