From af40e618111581c82fc44de922368a02208b499f Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 24 Jul 2024 15:11:54 +0200
Subject: [PATCH] chore: typo

---
 src/Lean/Util/Path.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Util/Path.lean b/src/Lean/Util/Path.lean
index 2d6b48fde035..6d1ba4c4074a 100644
--- 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