Skip to content

[Merged by Bors] - chore: rename pochhammer#6917

Closed
mo271 wants to merge 6 commits intomasterfrom
mo271/pochhammer
Closed

[Merged by Bors] - chore: rename pochhammer#6917
mo271 wants to merge 6 commits intomasterfrom
mo271/pochhammer

Conversation

@mo271
Copy link
Copy Markdown
Collaborator

@mo271 mo271 commented Sep 1, 2023 •
edited by jcommelin
Loading

We rename pochhammer to ascPochhammer to prepare adding descPochhammer.

Open in Gitpod

@mo271 mo271 mentioned this pull request Sep 1, 2023
Closed
1 task
@mo271 mo271 added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Sep 1, 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 Sep 1, 2023
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Sep 6, 2023

Thanks 🎉

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Sep 6, 2023
@mo271
Copy link
Copy Markdown
Collaborator Author

mo271 commented Sep 6, 2023

This will result in a merge conflict with #6897 and #6906. I'm happy to work them out

bors bot pushed a commit that referenced this pull request Sep 6, 2023
@mo271
chore: rename pochhammer (#6917)
67f18d4 
We rename `pochhammer` to `ascPochhammer`  to prepare adding `descPochhammer`.



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
chore: rename pochhammer (#6917)
dbad31c 
We rename `pochhammer` to `ascPochhammer`  to prepare adding `descPochhammer`.



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
chore: rename pochhammer (#6917)
9c5b745 
We rename `pochhammer` to `ascPochhammer`  to prepare adding `descPochhammer`.



Co-authored-by: Moritz Firsching <firsching@google.com>
@bors
Copy link
Copy Markdown

bors bot commented Sep 6, 2023

Build failed (retrying...):

@bors
Copy link
Copy Markdown

bors bot commented Sep 6, 2023

Canceled.

@Ruben-VandeVelde Ruben-VandeVelde added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed ready-to-merge This PR has been sent to bors. labels Sep 6, 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 Sep 7, 2023
@mo271
Copy link
Copy Markdown
Collaborator Author

mo271 commented Sep 7, 2023

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Sep 7, 2023

🔒 Permission denied

Existing reviewers: click here to make mo271 a reviewer

@mo271
Copy link
Copy Markdown
Collaborator Author

mo271 commented Sep 7, 2023

this should be ready to go again, the merge conflict was expected and is resolved now

@mo271 mo271 requested a review from jcommelin September 10, 2023 08:23
@mo271
Copy link
Copy Markdown
Collaborator Author

mo271 commented Sep 10, 2023

I think this should merge cleanly by now...

@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Sep 12, 2023

Thanks 🎉

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Sep 12, 2023
bors bot pushed a commit that referenced this pull request Sep 12, 2023
@mo271 @Ruben-VandeVelde
chore: rename pochhammer (#6917)
775b777 
We rename `pochhammer` to `ascPochhammer`  to prepare adding `descPochhammer`.



Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
@bors
Copy link
Copy Markdown

bors bot commented Sep 12, 2023

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Sep 12, 2023
@mo271 @Ruben-VandeVelde
chore: rename pochhammer (#6917)
ae1eb5e 
We rename `pochhammer` to `ascPochhammer`  to prepare adding `descPochhammer`.



Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
@bors
Copy link
Copy Markdown

bors bot commented Sep 12, 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 chore: rename pochhammer [Merged by Bors] - chore: rename pochhammer Sep 12, 2023
@bors bors bot closed this Sep 12, 2023
@bors bors bot deleted the mo271/pochhammer branch September 12, 2023 14:05
bors bot pushed a commit that referenced this pull request Sep 14, 2023
@mo271
feat: descPochhammer (#6918)
42093ba 
- [x] depends on: #6917 



Co-authored-by: Moritz Firsching <firsching@google.com>
kodyvajjha pushed a commit that referenced this pull request Sep 22, 2023
@mo271 @Ruben-VandeVelde @kodyvajjha
chore: rename pochhammer (#6917)
bc188ef 
We rename `pochhammer` to `ascPochhammer`  to prepare adding `descPochhammer`.



Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
kodyvajjha pushed a commit that referenced this pull request Sep 22, 2023
@mo271 @kodyvajjha
feat: descPochhammer (#6918)
14fcc87 
- [x] depends on: #6917 



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 Awaiting requested review from jcommelin

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@mo271 @jcommelin @Ruben-VandeVelde