Skip to content

[Merged by Bors] - feat: patch for std4#219#6622

Closed
fgdorais wants to merge 2 commits intomasterfrom
fgdorais-substring-coe
Closed

[Merged by Bors] - feat: patch for std4#219#6622
fgdorais wants to merge 2 commits intomasterfrom
fgdorais-substring-coe

Conversation

@fgdorais
Copy link
Copy Markdown
Collaborator

@fgdorais fgdorais commented Aug 17, 2023

@fgdorais fgdorais added WIP Work in progress blocked-by-batt-PR This PR depends on a PR to Batteries labels Aug 17, 2023
@ghost ghost added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Aug 17, 2023
@fgdorais fgdorais added awaiting-review and removed WIP Work in progress blocked-by-batt-PR This PR depends on a PR to Batteries labels Aug 17, 2023
@fgdorais fgdorais force-pushed the fgdorais-substring-coe branch from 7f2ec35 to e22dff1 Compare August 17, 2023 03:23
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 17, 2023
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 17, 2023
@ghost
Copy link
Copy Markdown

ghost commented Aug 17, 2023

@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Aug 17, 2023

Builds locally for me, so

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Aug 17, 2023
bors bot pushed a commit that referenced this pull request Aug 17, 2023
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Aug 17, 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 feat: patch for std4#219 [Merged by Bors] - feat: patch for std4#219 Aug 17, 2023
@bors bors bot closed this Aug 17, 2023
@bors bors bot deleted the fgdorais-substring-coe branch August 17, 2023 12:57
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