Skip to content

Conversation

hvitved
Copy link
Contributor

@hvitved hvitved commented Apr 20, 2022

We may as well give the optimizer these disjointness facts.

@github-actions github-actions bot added the Ruby label Apr 20, 2022
@hvitved hvitved marked this pull request as ready for review April 20, 2022 11:59
@hvitved hvitved requested a review from a team as a code owner April 20, 2022 11:59
@hvitved hvitved added the no-change-note-required This PR does not need a change note label Apr 20, 2022
@erik-krogh
Copy link
Contributor

LGTM, I might adopt it for JS/Python.

Have you done an evaluation?

@hvitved
Copy link
Contributor Author

hvitved commented Apr 20, 2022

Have you done an evaluation?

Nope, I will start one. I don't expect any changes, but better safe than sorry.

Copy link
Contributor

@nickrolfe nickrolfe left a comment

Choose a reason for hiding this comment

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

I didn't know you could do that! LGTM 👍

@erik-krogh
Copy link
Contributor

The evaluation showed no performance difference.
I'm merging. I'll look into making the same change for PY/JS.

@erik-krogh erik-krogh merged commit 8bd975a into github:main Apr 20, 2022
@hvitved hvitved deleted the ruby/api-graph-labels branch April 20, 2022 17:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
no-change-note-required This PR does not need a change note Ruby
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants