Skip to content
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.

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

Discouraged file path can be specified on the command line #97

Merged
merged 2 commits into from
Feb 19, 2023

Conversation

tirix
Copy link
Collaborator

@tirix tirix commented Feb 19, 2023

No description provided.

@digama0
Copy link
Member

digama0 commented Feb 19, 2023

Since regen_discouraged and output_discouraged are basically the same thing now, I combined them into one function and moved the file handling into the command line tool itself. Also the scope pass is not necessary for discouraged generation, so I made it optional and now it only takes 241ms to generate the discouraged file for set.mm.

@digama0 digama0 merged commit 3f3ff07 into metamath:main Feb 19, 2023
@tirix
Copy link
Collaborator Author

tirix commented Feb 19, 2023

Ok for the changes!
I just think the dummy closure is maybe a bit hard to read. I wanted to propose a small change but I was just one minute too slow, so I created a new PR, #98

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