lean4-htt/src/shell
Joachim Breitner 0471319b5a
chore: tests: use filenames as test names (#11302)
This PR renames the CTests tests to use filenames as test names. So
instead of
```
        2080 - leanruntest_issue5767.lean (Failed)
```
we get
```
        2080 - tests/lean/run/issue5767.lean (Failed)
```
which allows Ctrl-Click’ing on them in the VSCode terminal.
2025-11-21 12:40:58 +00:00
..
app.manifest
CMakeLists.txt chore: tests: use filenames as test names (#11302) 2025-11-21 12:40:58 +00:00
lean.cpp
lean_js.cpp
manifest.rc
mk_lean_sh.sh