Zulip Chat Archive
Stream: general
Topic: lean path in vscode
Jakob von Raumer (Oct 08 2018 at 16:38):
VSCode doesn't seem to use the leanpkg.path path when I'm in a directory? I have a dependency in a package, but it cannot be resolved :(
Gabriel Ebner (Oct 08 2018 at 16:39):
Only the leanpkg.path from the root directory.
Jakob von Raumer (Oct 08 2018 at 16:39):
The root dir of the project?
Gabriel Ebner (Oct 08 2018 at 16:39):
The directory you've opened in vscode.
Jakob von Raumer (Oct 08 2018 at 16:39):
Ah, forgot about that, thanks :)
Last updated: Dec 20 2023 at 11:08 UTC