Today's updates #106

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Merged

cscheid merged 2 commits into main from updates/2025-11-13

Nov 13, 2025

Contributor

cscheid commented Nov 13, 2025 •

edited

Loading

Much improved error pruning; we no longer emit a billion errors per file
emoji support
## unnumbered section {-} support
many other small grammar fixes

cscheid added 2 commits

November 13, 2025 15:20


          make tests pass

35eb6f1

fix

e5d13e3

cscheid merged commit d096911 into main

2 checks passed

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet