chore: typo

leanprover · Jul 24, 2024 · af40e61 · af40e61
1 parent 1758b37
commit af40e61
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Lean/Util/Path.lean b/src/Lean/Util/Path.lean
@@ -113,7 +113,7 @@ partial def findOLean (mod : Name) : IO FilePath := do
     let pkg := FilePath.mk <| mod.getRoot.toString (escape := false)
     let mut msg := s!"unknown module prefix '{pkg}'
 
-No directory '{pkg}' or file '{pkg}.lean' in the search path entries:
+No directory '{pkg}' or file '{pkg}.olean' in the search path entries:
 {"\n".intercalate <| sp.map (·.toString)}"
     throw <| IO.userError msg