fix bad merge

kim-em · kim-em · commit e3ff8212d4d1 · 2025-05-29T21:22:25.000+10:00
diff --git a/MathlibTest/DirectoryDependencyLinter/Test.lean b/MathlibTest/DirectoryDependencyLinter/Test.lean
@@ -7,19 +7,19 @@ import Mathlib.Init
 import Qq
 import Mathlib.Util.AssertExists
 
--- /--
--- warning: Module MathlibTest.DirectoryDependencyLinter.Test depends on Mathlib.Util.AssertExists,
--- but is only allowed to import modules starting with one of [Mathlib.Lean].
--- Note: module Mathlib.Util.AssertExists is directly imported by this module
--- note: this linter can be disabled with `set_option linter.directoryDependency false`
--- ---
--- warning: The module doc-string for a file should be the first command after the imports.
--- Please, add a module doc-string before `/-!# Tests for the `directoryDependency` linter
--- -/
--- `.
--- note: this linter can be disabled with `set_option linter.style.header false`
--- -/
--- #guard_msgs in
+/--
+warning: Module MathlibTest.DirectoryDependencyLinter.Test depends on Mathlib.Util.AssertExists,
+but is only allowed to import modules starting with one of [Mathlib.Lean].
+Note: module Mathlib.Util.AssertExists is directly imported by this module
+note: this linter can be disabled with `set_option linter.directoryDependency false`
+---
+warning: The module doc-string for a file should be the first command after the imports.
+Please, add a module doc-string before `/-!# Tests for the `directoryDependency` linter
+-/
+`.
+note: this linter can be disabled with `set_option linter.style.header false`
+-/
+#guard_msgs in
 set_option linter.style.header true in
 
 /-!
