-
Notifications
You must be signed in to change notification settings - Fork 193
More benchmarks #1899
New issue
Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? # to your account
More benchmarks #1899
Conversation
a894bb5
to
b9e9274
Compare
616d644
to
5407124
Compare
For some reasons the benchmarks results don’t show in the logs. |
Are you looking at the right place? |
Apparently not. I was tripped on the fact that clicking on a benchmark set resets the PR selection. |
Yes, that's confusing. |
f88c4b7
to
a3409b3
Compare
There seems to still be ppxlib-related issues in the benchmarking CI… |
5dad0d2
to
33c00a6
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This looks great to me. Should we wait for the benchmarking server to work again before merging?
Let's wait. I have not seen the result of my latest changes. |
(The benchmarking server looks like it’s in a better state now.) |
33c00a6
to
32f4070
Compare
Some benchmarks results have “?” as a result still. |
I think this is because the result or the metric has been renamed. |
In that case, feel free to merge. |
32f4070
to
cf4de97
Compare
No description provided.