Zulip Chat Archive

Stream: new members

Topic: path


Alex Zhang (Jul 12 2021 at 10:34):

In the leanpkg.path file of my project, I found

builtin_path
path _target/deps/mathlib/src
path _target/deps/lean-gptf/src
path ./src

What is the third path path ./src to? (This may be a trivial CS question.. please forgive that I am not a CS person)

Eric Wieser (Jul 12 2021 at 11:05):

That should be where your own code is

Eric Wieser (Jul 12 2021 at 11:05):

You're looking at whatever/myproject/leanpkg.path, that line refers to whatever/myproject/src

Alex Zhang (Jul 12 2021 at 11:39):

Thanks, Eric!


Last updated: Dec 20 2023 at 11:08 UTC