VS Code go-to-definition

Stream: new members

[Dominique Danco]

When I'm in my project folder in VS code, I'm able to use 'Go to definition' to get to the proper location inside .elan/toolchains/leanprover--lean4---nightly[...]/[...]/lean, but once I'm inside those folders, I can no longer use Go to def. Does anyone know how to fix this? Thanks

[Arthur Paulino]

I reported this problem here

[Dominique Danco]

thanks

[Arthur Paulino]

@Dominique Danco I just noticed that it's working again with the extension version v0.0.68
Does it work for you?

[Dominique Danco]

It does!