Skip to content

Conversation

@maxwell3025
Copy link
Contributor

This PR changes rmdir*(..., {recursive: true}) to rm*(..., {recursive: true}) as recommended in DEP0147.

This removes clutter in the testing suite output and prevents errors when the feature is removed by NodeJS.

@mhuisi
Copy link
Collaborator

mhuisi commented Dec 19, 2025

Thanks! :-)

@mhuisi mhuisi changed the title fix: change recursive rmdir to rm to fix DEP0147 warning test: change recursive rmdir to rm to fix DEP0147 warning Dec 19, 2025
@mhuisi mhuisi merged commit f23cef6 into leanprover:master Dec 19, 2025
2 checks passed
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.

2 participants