fix: import hint

2021-08-17 11:14:42 +02:00 · 2021-08-17 11:14:42 +02:00 · 94437bcfbb
commit 94437bcfbb
parent 9d24f614fa
1 changed files with 1 additions and 1 deletions
--- 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