lean4-htt/tests/lake
Mac Malone 6f409e0eea
fix: lake: --no-build exit code w/ release fetch (#12142)
This PR fixes a bug introduced in #12086 where a `lake build :release
--no-build` would exit with code 1 rather than the `--no-build ` code 3.
Now both the bug from #12086 and this bug are fixed.
2026-01-24 17:03:07 +00:00
..
examples chore: lake: mv targets test to tests (#11592) 2025-12-11 09:28:44 +00:00
tests fix: lake: --no-build exit code w/ release fetch (#12142) 2026-01-24 17:03:07 +00:00
.gitattributes
.gitignore
build.sh
clean-build.sh
lakefile.toml feat: module system is no longer experimental (#11637) 2025-12-12 21:20:26 +00:00
Makefile
time-build.sh