Skip to content

[Merged by Bors] - chore: avoid subst by rfl#8145

Closed
mo271 wants to merge 1 commit intomasterfrom
mo271/rfl_porting_note
Closed

[Merged by Bors] - chore: avoid subst by rfl#8145
mo271 wants to merge 1 commit intomasterfrom
mo271/rfl_porting_note

Conversation

@mo271
Copy link
Copy Markdown
Collaborator

@mo271 mo271 commented Nov 3, 2023

No description provided.

@mo271 mo271 added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Nov 3, 2023
@mo271 mo271 mentioned this pull request Nov 3, 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 Nov 3, 2023
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Nov 3, 2023
bors bot pushed a commit that referenced this pull request Nov 3, 2023
Co-authored-by: Moritz Firsching <firsching@google.com>
@bors
Copy link
Copy Markdown

bors bot commented Nov 3, 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: avoid subst by rfl [Merged by Bors] - chore: avoid subst by rfl Nov 3, 2023
@bors bors bot closed this Nov 3, 2023
@bors bors bot deleted the mo271/rfl_porting_note branch November 3, 2023 10:44
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