Skip to content

Conversation

@joshlf
Copy link
Member

@joshlf joshlf commented Oct 5, 2023

No description provided.

@joshlf joshlf requested a review from jswrenn October 5, 2023 16:26
@joshlf joshlf enabled auto-merge October 5, 2023 16:26
@joshlf joshlf added this pull request to the merge queue Oct 5, 2023
@joshlf joshlf removed this pull request from the merge queue due to a manual request Oct 5, 2023
@joshlf
Copy link
Member Author

joshlf commented Oct 5, 2023

I'm going to avoid merging this for now to give #469 a chance to put up its own roll PR.

@joshlf
Copy link
Member Author

joshlf commented Oct 5, 2023

Here's the PR generated by #469: #471

@joshlf
Copy link
Member Author

joshlf commented Oct 5, 2023

Closing in favor of #471.

@joshlf joshlf closed this Oct 5, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants