lean4-htt/.claude
Mac Malone 24bef91f9a
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.
2026-04-25 04:36:08 +00:00
..
commands chore: add safety notes to release command (#13225) 2026-04-01 05:01:00 +00:00
skills chore: fix profiler shebang and add profiling skill (#12519) 2026-03-01 07:09:33 +00:00
CLAUDE.md test: tests/lake/run_test.sh (#13501) 2026-04-25 04:36:08 +00:00
settings.json chore: enable leanprover/skills plugin for Claude Code (#12609) 2026-02-20 12:35:32 +00:00