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

Clean up some stuff around comments #1016

Merged
merged 5 commits into from
Apr 25, 2023
Merged

Clean up some stuff around comments #1016

merged 5 commits into from
Apr 25, 2023

Conversation

brandonchinn178
Copy link
Collaborator

Some clean up broken out from #933

@brandonchinn178 brandonchinn178 requested a review from amesgen April 25, 2023 00:35
@brandonchinn178 brandonchinn178 changed the title Cleanup some stuff around comments Clean up some stuff around comments Apr 25, 2023
amesgen
amesgen approved these changes Apr 25, 2023
View reviewed changes
Copy link
Member

@amesgen amesgen left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks, looks good, especially the 1. and 5. commit 👍

@mrkkrp mrkkrp merged commit 6545081 into tweag:master Apr 25, 2023
@mrkkrp
Copy link
Member

mrkkrp commented Apr 25, 2023

Thanks!

@brandonchinn178 brandonchinn178 deleted the cleanup branch April 25, 2023 15:04
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@amesgen amesgen amesgen approved these changes

@mrkkrp mrkkrp mrkkrp approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@brandonchinn178 @mrkkrp @amesgen