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 control flow #98

Merged
merged 1 commit into from
Feb 19, 2023
Merged

Discouraged control flow #98

merged 1 commit into from
Feb 19, 2023

Conversation

tirix
Copy link
Collaborator

@tirix tirix commented Feb 19, 2023

I prefer this control flow for discouraged in main.rs, I think it's clearer than the dummy closure.
I wanted to push this on the previous pull request but I was just one minute too slow!

@digama0
Copy link
Member

digama0 commented Feb 19, 2023

heh, I was looking at that and thinking of exactly the same change :)

@digama0 digama0 merged commit 4594695 into metamath:main Feb 19, 2023
@tirix tirix deleted the discouraged-path2 branch February 19, 2023 18:46
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