Zulip Chat Archive

Stream: general

Topic: lean path in vscode


view this post on Zulip 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 :(

view this post on Zulip Gabriel Ebner (Oct 08 2018 at 16:39):

Only the leanpkg.path from the root directory.

view this post on Zulip Jakob von Raumer (Oct 08 2018 at 16:39):

The root dir of the project?

view this post on Zulip Gabriel Ebner (Oct 08 2018 at 16:39):

The directory you've opened in vscode.

view this post on Zulip Jakob von Raumer (Oct 08 2018 at 16:39):

Ah, forgot about that, thanks :)


Last updated: May 14 2021 at 12:18 UTC