Skip to content

Commit 8568f33

Browse files
committed
chore: restore initialize test for privateModule linter with correct wording
1 parent 7a5e5b4 commit 8568f33

1 file changed

Lines changed: 1 addition & 3 deletions

File tree

MathlibTest/PrivateModuleLinter/initialize.lean

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2,11 +2,9 @@ module
22

33
import Mathlib.Tactic.Linter.PrivateModule
44

5-
set_option linter.privateModule false -- Changed in nightly-testing, as this test no longer works.
6-
75
open Lean
86

9-
-- Should not fire, since `initialize` creates a genuinely public declaration.
7+
-- Should not fire, since `initialize` has effects downstream despite creating a private decl here.
108
initialize pure ()
119

1210
/- Check that we have indeed created a declaration, and aren't not linting just due to being an

0 commit comments

Comments
 (0)