Skip to content

Commit d145b9f

Browse files
tydeutydeu
authored
chore: lake: mv targets test to tests (#11592)
This PR moves Lake's `tests/lake/examples/targets` test from `examples` to `tests` (and thus disabling it by default). It is being [flaky](https://github.com/leanprover/lean4/actions/runs/20111185289/attempts/1) for some unknown reason, so I am disabling until I have a better opportunity to debug it.
1 parent 05a8124 commit d145b9f

File tree

11 files changed

+0
-0
lines changed

11 files changed

+0
-0
lines changed

tests/lake/examples/targets/clean.sh renamed to tests/lake/tests/targets/clean.sh

File renamed without changes.

tests/lake/examples/targets/lakefile.lean renamed to tests/lake/tests/targets/lakefile.lean

File renamed without changes.

tests/lake/examples/targets/src/Bar.lean renamed to tests/lake/tests/targets/src/Bar.lean

File renamed without changes.

tests/lake/examples/targets/src/Baz.lean renamed to tests/lake/tests/targets/src/Baz.lean

File renamed without changes.

tests/lake/examples/targets/src/Foo.lean renamed to tests/lake/tests/targets/src/Foo.lean

File renamed without changes.

tests/lake/examples/targets/src/Foo/Bar.lean renamed to tests/lake/tests/targets/src/Foo/Bar.lean

File renamed without changes.

tests/lake/examples/targets/src/Foo/Baz.lean renamed to tests/lake/tests/targets/src/Foo/Baz.lean

File renamed without changes.

tests/lake/examples/targets/src/a.lean renamed to tests/lake/tests/targets/src/a.lean

File renamed without changes.

tests/lake/examples/targets/src/b.lean renamed to tests/lake/tests/targets/src/b.lean

File renamed without changes.

tests/lake/examples/targets/src/c.lean renamed to tests/lake/tests/targets/src/c.lean

File renamed without changes.

0 commit comments

Comments
 (0)