Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - doc(order/succ_pred/basic): fix typo #12501

Closed
wants to merge 1 commit into from

Conversation

meithecatte
Copy link
Collaborator


Open in Gitpod

@meithecatte meithecatte added the easy < 20s of review time. See the lifecycle page for guidelines. label Mar 7, 2022
@vihdzp vihdzp added the docs This PR is about documentation label Mar 8, 2022
@kim-em kim-em added the awaiting-review The author would like community review of the PR label Mar 8, 2022
@kim-em
Copy link
Collaborator

kim-em commented Mar 8, 2022

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Mar 8, 2022
bors bot pushed a commit that referenced this pull request Mar 8, 2022
@bors
Copy link

bors bot commented Mar 8, 2022

This PR was included in a batch that was canceled, it will be automatically retried

bors bot pushed a commit that referenced this pull request Mar 8, 2022
@bors
Copy link

bors bot commented Mar 8, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title doc(order/succ_pred/basic): fix typo [Merged by Bors] - doc(order/succ_pred/basic): fix typo Mar 8, 2022
@bors bors bot closed this Mar 8, 2022
@bors bors bot deleted the succ-pred-typo branch March 8, 2022 10:39
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
docs This PR is about documentation easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants