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

Fix typo #534

Merged
merged 3 commits into from
Dec 8, 2023
Merged

Fix typo #534

merged 3 commits into from
Dec 8, 2023

Conversation

LilithHafner
Copy link
Member

No description provided.

@DilumAluthge
Copy link
Member

bors merge

@ericphanson
Copy link
Member

Need merge queue :(

@DilumAluthge
Copy link
Member

😭

@DilumAluthge
Copy link
Member

Well, at least we don't enforce Codecov as a required status check on this repo. That might make this easier.

@ericphanson ericphanson enabled auto-merge December 7, 2023 23:43
@ericphanson
Copy link
Member

I clicked merge-when-ready but it seems to be waiting on integration tests. I'll merge in main so they run and get skipped.

@ericphanson ericphanson added this pull request to the merge queue Dec 8, 2023
Merged via the queue into JuliaRegistries:master with commit 10a0449 Dec 8, 2023
11 checks passed
@LilithHafner LilithHafner deleted the patch-1 branch December 8, 2023 17:21
@LilithHafner
Copy link
Member Author

This was a surprisingly involved pull request, considering the diff. :)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@DilumAluthge DilumAluthge DilumAluthge 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.
3 participants
@LilithHafner @DilumAluthge @ericphanson