max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: lake: mv targets test to tests (#11592)

Browse source 
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.
This commit is contained in:
Mac Malone 2025-12-11 04:28:44 -05:00 • committed by GitHub
parent 05a81248df
commit d145b9f8ee
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
11 changed files with 0 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files