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

Update milestones #100

Merged
merged 1 commit into from
May 29, 2023
Merged

Update milestones #100

merged 1 commit into from
May 29, 2023

Conversation

rkuris
Copy link
Collaborator

@rkuris rkuris commented May 26, 2023

Added metrics to the green and seasoned milestones per discussions.

Added metrics to the green and seasoned milestones per discussions.
@rkuris rkuris self-assigned this May 26, 2023
Copy link
Contributor

@richardpringle richardpringle left a comment

Choose a reason for hiding this comment

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

🥇

- [ ] Be able to propose a batch against the existing committed revision, or
propose a batch against any existing proposed revision.
- [ ] Be able to quickly commit a batch that has been proposed. Note that this
invalidates all other proposals that are not children of the committed proposed batch.
- [ ] Add metric reporting
Copy link
Contributor

Choose a reason for hiding this comment

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

Do you want to be more specific and say "as a part of benchmarking" or something like that?

In any case this is good, we can be more specific later if you want to just merge this now.

@rkuris rkuris merged commit ffd2b6a into main May 29, 2023
@rkuris rkuris deleted the rkuris/metrics-in-milestones branch May 29, 2023 17:26
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