lean4-htt/tests/lake/examples/deps
Mac Malone 41ecccec6d
feat: lake: hoist compiled configurations (#13683)
This PR moves the compiled Lake configurations (e.g., `lakefile.olean`)
from the package's `.lake/config` directory to the workspace's
`.lake/config`. This removes a potential source contention between
workspaces sharing a dependency.
2026-05-08 18:00:37 +00:00
..
a
b
bar
foo
root
clean.sh
test.sh feat: lake: hoist compiled configurations (#13683) 2026-05-08 18:00:37 +00:00