How to require local repo in a project

Stream: general

[Segev Elazar Mittelman]

I was wondering how to require a local lean project in another project using the absolute path? Once I have that, is there anything to do besides lake update?

Here's what I have:

require plausible from "/home" / "plausible"

Here's what I get when I try importing Plausible.Chamelean

stderr:
warning: manifest out of date: source kind (git/path) of dependency 'plausible' changed; use `lake update plausible` to update it
✖ [267/268] Running Plausible.Chamelean
error: no such file or directory (error code: 2)

This is the result of trying lake update plausible

info: toolchain not updated; already up-to-date

Thank you!
-Segev

[Kim Morrison]

Try with just a single string? Verify that the path does actually exist?