Skip to content

Commit e0f9620

Browse files
authored
chore: typo in error message (#11262)
1 parent 5cc0a10 commit e0f9620

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Lean/Environment.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2002,7 +2002,7 @@ partial def importModulesCore
20022002
for i in imports do
20032003
if let some mod := (← get).moduleNameMap[i.module]?.bind (·.mainModule?) then
20042004
if !mod.isModule then
2005-
throw <| IO.userError s!"cannot import non`-module` {i.module} from `module`"
2005+
throw <| IO.userError s!"cannot import non-`module` {i.module} from `module`"
20062006
/-
20072007
When the module system is disabled for the root, we import all transitively referenced modules and
20082008
ignore any module system annotations on the way.

0 commit comments

Comments
 (0)