We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 5e5554a commit d378639Copy full SHA for d378639
MathlibTest/DeprecatedModuleAllTest.lean
@@ -9,6 +9,7 @@ warning: Testing public import deprecation
9
import Mathlib.Tactic.Linter.DocPrime
10
import Mathlib.Tactic.Linter.DocString
11
12
+
13
Note: This linter can be disabled with `set_option linter.deprecated.module false`
14
-/
15
#guard_msgs in
0 commit comments