From 94437bcfbbc1e161296c8c5347aed7da20656405 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 17 Aug 2021 11:14:42 +0200
Subject: [PATCH] fix: import hint

---
 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 a6c6ae8434..89400a8a51 100644
--- a/src/Lean/Util/Path.lean
+++ b/src/Lean/Util/Path.lean
@@ -82,7 +82,7 @@ partial def findOLean (mod : Name) : IO FilePath := do
     let pkg := FilePath.mk mod.getRoot.toString
     let mut msg := s!"unknown package '{pkg}'"
     let rec maybeThisOne dir := do
-      if ← (pkg / dir).isDir then
+      if ← (dir / pkg).isDir then
         return some s!"\nYou might need to open '{dir}' as a workspace in your editor"
       if let some dir ← dir.parent then
         maybeThisOne dir