Skip to content

[Merged by Bors] - chore: tidy Data/Complex/Basic#2844

Closed
ChrisHughes24 wants to merge 1 commit intomasterfrom
tidy_complex
Closed

[Merged by Bors] - chore: tidy Data/Complex/Basic#2844
ChrisHughes24 wants to merge 1 commit intomasterfrom
tidy_complex

Conversation

@ChrisHughes24
Copy link
Copy Markdown
Member


Open in Gitpod

@ChrisHughes24 ChrisHughes24 added awaiting-review easy < 20s of review time. See the lifecycle page for guidelines. labels Mar 13, 2023
@fpvandoorn
Copy link
Copy Markdown
Member

Thanks!

bors merge

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

bors bot commented Mar 13, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore: tidy Data/Complex/Basic [Merged by Bors] - chore: tidy Data/Complex/Basic Mar 13, 2023
@bors bors bot closed this Mar 13, 2023
@bors bors bot deleted the tidy_complex branch March 13, 2023 13:02
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants