Skip to content

[Merged by Bors] - chore: revert #7703#7710

Closed
mattrobball wants to merge 1 commit intomasterfrom
mrb/revert_7703
Closed

[Merged by Bors] - chore: revert #7703#7710
mattrobball wants to merge 1 commit intomasterfrom
mrb/revert_7703

Conversation

@mattrobball
Copy link
Copy Markdown
Contributor

This reverts commit 26eb2b0.


Open in Gitpod

@mattrobball mattrobball added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Oct 16, 2023
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Oct 16, 2023
@j-loreaux
Copy link
Copy Markdown
Contributor

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Oct 16, 2023
bors bot pushed a commit that referenced this pull request Oct 16, 2023
This reverts commit 26eb2b0.
@bors
Copy link
Copy Markdown

bors bot commented Oct 16, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title chore: revert #7703 [Merged by Bors] - chore: revert #7703 Oct 16, 2023
@bors bors bot closed this Oct 16, 2023
@bors bors bot deleted the mrb/revert_7703 branch October 16, 2023 20:26
kim-em added a commit that referenced this pull request Oct 17, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants