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.

Sign up for GitHub

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

Jump to bottom

Rename workspace to buffer in sorting #45711

Merged
merged 1 commit into from
Jun 29, 2022
Merged

Rename workspace to buffer in sorting #45711

merged 1 commit into from
Jun 29, 2022

Conversation

LilithHafner
Copy link
Member

See discussion in #45330

@LilithHafner
Copy link
Member Author

Let's actually hold off on this until after #45211

@ViralBShah ViralBShah marked this pull request as draft June 17, 2022 01:46
@LilithHafner LilithHafner marked this pull request as ready for review June 22, 2022 11:34
@LilithHafner
Copy link
Member Author

LilithHafner commented Jun 22, 2022 •
edited
Loading

I thought #45211 was going to merge on the 16th, but since that's taking a while, we can proceed here. The merge conflict in #45211 will only be a couple of lines.

@LilithHafner LilithHafner force-pushed the rename-workspace-to-buffer branch from c98abb0 to cf0c03b Compare June 22, 2022 14:46
@LilithHafner
Copy link
Member Author

Rebased on top of #45211, handling merge conflicts. Looks ready to merge to me.

@LilithHafner
Copy link
Member Author

Bump, I think the CI failures are unrelated

@oscardssmith oscardssmith merged commit 82fcea4 into JuliaLang:master Jun 29, 2022
@LilithHafner LilithHafner deleted the rename-workspace-to-buffer branch June 30, 2022 13:36
@LilithHafner LilithHafner added the sorting Put things in order label Jul 19, 2022
pcjentsch pushed a commit to pcjentsch/julia that referenced this pull request Aug 18, 2022
@LilithHafner @pcjentsch
rename workspace to buffer (JuliaLang#45711)
16e8b37 
Co-authored-by: Lilith Hafner <Lilith.Hafner@gmail.com>
@LilithHafner LilithHafner mentioned this pull request Oct 15, 2022
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@oscardssmith oscardssmith oscardssmith approved these changes

Assignees
No one assigned
Labels
sorting Put things in order
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@LilithHafner @oscardssmith