commit: 24bef91f9a20a45f074729e869461d374687de1c

[log]
author: Mac Malone <tydeu@hatpress.net>

Sat Apr 25 00:36:08 2026 -0400
committer: GitHub <noreply@github.com>

Sat Apr 25 04:36:08 2026 +0000
tree: 038948b9023cd92495f461a7b8518aa069914026
parent: 09fabf3c3961ea33023b123fd8cd0517f7e2423c [diff]

test: `tests/lake/run_test.sh` (#13501)

This PR removes the Makefile-based Lake test runner and replaces it with
`run_test.sh` and `run_clean.sh`. These are still not designed for use
with the `with_*.sh` runners, but this a step closer to that
eventuality.

It also adds a line to `CLAUDE.md` informing Claude how to build and run
a single Lake test.

.claude/CLAUDE.md[diff]
tests/lake/Makefile[Deleted - diff]
tests/lake/build.sh[Deleted - diff]
tests/lake/clean-build.sh[Deleted - diff]
tests/lake/run_clean.sh[Added - diff]
tests/lake/run_test.sh[Added - diff]
tests/lake/time-build.sh[Deleted - diff]

7 files changed

tree: 038948b9023cd92495f461a7b8518aa069914026

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.