lean4-htt/tests/docparse/blocks_0039.txt
Garmelon a3cb39eac9
chore: migrate more tests to new test suite (#12809)
This PR migrates most remaining tests to the new test suite. It also
completes the migration of directories like `tests/lean/run`, meaning
that PRs trying to add tests to those old directories will now fail.
2026-03-06 16:52:01 +00:00

7 lines
No EOL
137 B
Text

Attention:
Here is a paragraph with an unterminated `code block
that would be super annoying without error recovery in the
parser.
Yep.