Skip to content
This repository has been archived by the owner on Apr 4, 2023. It is now read-only.

Rename the search benchmarks #298

Merged
merged 2 commits into from
Jul 29, 2021
Merged

Rename the search benchmarks #298

merged 2 commits into from
Jul 29, 2021

Conversation

irevoire
Copy link
Member

And fix a bug. As always, I was not closing the env.

@irevoire irevoire requested a review from Kerollmops July 29, 2021 15:30
Kerollmops
Kerollmops approved these changes Jul 29, 2021
View reviewed changes
Copy link
Member

@Kerollmops Kerollmops left a comment

Choose a reason for hiding this comment

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

Nice, thank you!
bors merge

@bors
Copy link
Contributor

bors bot commented Jul 29, 2021

Build succeeded:

@bors bors bot merged commit cb45a10 into main Jul 29, 2021
@bors bors bot deleted the bench/search branch July 29, 2021 15:56
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@Kerollmops Kerollmops Kerollmops 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.
2 participants
@irevoire @Kerollmops