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
[Merged by Bors] - chore(Data/List/Enum): move from Basic
#11697
Conversation
urkud
commented
Mar 26, 2024
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.
I'm not sure if this qualifies as "easy", given Github's interface - I checked locally that this is purely code motion and import changes. Looks good to me.
Thank you for doing this!
OK, removed |
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.
bors merge
I'll take @grunweg's word for it that this is a move with no other changes
Build failed (retrying...): |
Build failed (retrying...): |
Build failed (retrying...): |
Build failed: |
Let me fix the build |
@eric-wieser If I see correctly, this is off the bors queue. Can you approve again, if you agree with the changes? |
bors r+ |
Pull request successfully merged into master. Build succeeded: |
Basic
Basic