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.

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

Tidy up FLT.lean #188

Merged
merged 1 commit into from
Oct 31, 2024
Merged

Tidy up FLT.lean #188

merged 1 commit into from
Oct 31, 2024

Conversation

kbuzzard
Copy link
Collaborator

@kbuzzard kbuzzard commented Oct 31, 2024 •
edited by github-actions bot
Loading

closes #52

Closes #52

@kbuzzard kbuzzard mentioned this pull request Oct 31, 2024
Closed
@kbuzzard
Copy link
Collaborator Author

Oh lol I didn't know that was added automatically :-)

@kbuzzard
Copy link
Collaborator Author

awaiting-review

@kbuzzard
Copy link
Collaborator Author

Thanks!

@kbuzzard kbuzzard merged commit 657fbc5 into main Oct 31, 2024
1 check passed
@kbuzzard kbuzzard deleted the FLT-tidy branch October 31, 2024 19:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
awaiting-review
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

TODO: make FLT.lean more interesting
1 participant
@kbuzzard