path

Stream: new members

[Alex Zhang]

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]

That should be where your own code is

[Eric Wieser]

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

[Alex Zhang]

Thanks, Eric!