Skip to content

Remove file-utils.ts#342

Closed
DikieDick wants to merge 215 commits intomainfrom
fix/remove-file-utils
Closed

Remove file-utils.ts#342
DikieDick wants to merge 215 commits intomainfrom
fix/remove-file-utils

Conversation

@DikieDick
Copy link
Copy Markdown
Contributor

Description

Short description for this Pull Request.

Changes

Brief summary of relevant changes.

Testing this PR

Please explain how we can test this Pull Request.
What should we watch out for and how can we automatically test this, if possible.

XyntaxCS and others added 30 commits April 8, 2025 12:44
GitLuckier and others added 28 commits March 21, 2026 18:11
Fix proof bar turning green prematurely in Lean (closes #313, #316)
Update @impermeable/codemirror-lang-verbose package
…package

updated lean symbol generation to be based on the npm package
@DikieDick DikieDick changed the title Remove `file-utils Remove file-utils.ts Apr 13, 2026
@DikieDick DikieDick closed this Apr 13, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

8 participants