Skip to content

[Merged by Bors] - feat: Monic pochhammer#6906

Closed
mo271 wants to merge 2 commits intomasterfrom
mo271/monic_pochhammer
Closed

[Merged by Bors] - feat: Monic pochhammer#6906
mo271 wants to merge 2 commits intomasterfrom
mo271/monic_pochhammer

Conversation

@mo271
Copy link
Copy Markdown
Collaborator

@mo271 mo271 commented Aug 31, 2023

Open in Gitpod

@mo271 mo271 added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Aug 31, 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 Aug 31, 2023
@mo271 mo271 mentioned this pull request Sep 2, 2023
Closed
1 task
jcommelin
jcommelin approved these changes Sep 6, 2023
View reviewed changes
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 Sep 6, 2023
@mo271 mo271 mentioned this pull request Sep 6, 2023
Closed
@bors
Copy link
Copy Markdown

bors bot commented Sep 6, 2023

Merge conflict.

@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 6, 2023
@ChrisHughes24 ChrisHughes24 added awaiting-author A reviewer has asked the author a question or requested changes. and removed ready-to-merge This PR has been sent to bors. labels Sep 6, 2023
@ChrisHughes24
Copy link
Copy Markdown
Member

ChrisHughes24 commented Sep 6, 2023

Merge after the conflict is resolved

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Sep 6, 2023

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

@github-actions github-actions bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Sep 6, 2023
@mo271
Copy link
Copy Markdown
Collaborator Author

mo271 commented Sep 6, 2023

bors r+

@bors
Copy link
Copy Markdown

bors bot commented Sep 6, 2023

👎 Rejected by label

@mo271 mo271 added awaiting-review and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) awaiting-review awaiting-author A reviewer has asked the author a question or requested changes. labels Sep 6, 2023
@mo271
Copy link
Copy Markdown
Collaborator Author

mo271 commented Sep 6, 2023

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Sep 6, 2023

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

@mo271
Copy link
Copy Markdown
Collaborator Author

mo271 commented Sep 6, 2023

bors r+

bors bot pushed a commit that referenced this pull request Sep 6, 2023
@mo271
feat: Monic pochhammer (#6906)
a988e17 
Co-authored-by: Moritz Firsching <firsching@google.com>
@bors
Copy link
Copy Markdown

bors bot commented Sep 6, 2023

Build failed (retrying...):

  • Build

bors bot pushed a commit that referenced this pull request Sep 6, 2023
@mo271
feat: Monic pochhammer (#6906)
bd3b2ef 
Co-authored-by: Moritz Firsching <firsching@google.com>
@bors
Copy link
Copy Markdown

bors bot commented Sep 6, 2023

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Sep 6, 2023
@mo271
feat: Monic pochhammer (#6906)
5f6506b 
Co-authored-by: Moritz Firsching <firsching@google.com>
@bors
Copy link
Copy Markdown

bors bot commented Sep 6, 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: Monic pochhammer [Merged by Bors] - feat: Monic pochhammer Sep 6, 2023
@bors bors bot closed this Sep 6, 2023
@bors bors bot deleted the mo271/monic_pochhammer branch September 6, 2023 17:13
ebab pushed a commit that referenced this pull request Sep 11, 2023
@mo271 @ebab
feat: Monic pochhammer (#6906)
b51d1e1 
Co-authored-by: Moritz Firsching <firsching@google.com>
kodyvajjha pushed a commit that referenced this pull request Sep 22, 2023
@mo271 @kodyvajjha
feat: Monic pochhammer (#6906)
1add2ce 
Co-authored-by: Moritz Firsching <firsching@google.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin approved these changes

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer).

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@mo271 @ChrisHughes24 @jcommelin