Skip to content

[Merged by Bors] - feat(List/MinMax): maximum_of_length_pos#6115

Closed
kim-em wants to merge 5 commits intomasterfrom
maximum_of_length_pos
Closed

[Merged by Bors] - feat(List/MinMax): maximum_of_length_pos#6115
kim-em wants to merge 5 commits intomasterfrom
maximum_of_length_pos

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Jul 24, 2023


Open in Gitpod

@kim-em kim-em added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jul 24, 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 Jul 25, 2023
Copy link
Copy Markdown
Contributor

@ocfnash ocfnash 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 d+

@bors
Copy link
Copy Markdown

bors bot commented Jul 29, 2023

✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Jul 29, 2023
kim-em and others added 2 commits July 30, 2023 13:40
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Jul 30, 2023

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jul 30, 2023
bors bot pushed a commit that referenced this pull request Jul 30, 2023
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Jul 30, 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(List/MinMax): maximum_of_length_pos [Merged by Bors] - feat(List/MinMax): maximum_of_length_pos Jul 30, 2023
@bors bors bot closed this Jul 30, 2023
@bors bors bot deleted the maximum_of_length_pos branch July 30, 2023 04:56
kim-em added a commit that referenced this pull request Aug 2, 2023
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
kim-em added a commit that referenced this pull request Aug 14, 2023
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). 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