Skip to content

[Merged by Bors] - chore: rm @simp from factorial#7078

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

[Merged by Bors] - chore: rm @simp from factorial#7078
mo271 wants to merge 2 commits intomasterfrom
mo271/no_simp_factorial

Conversation

@mo271
Copy link
Copy Markdown
Collaborator

@mo271 mo271 commented Sep 10, 2023

Open in Gitpod

@mo271 mo271 mentioned this pull request Sep 10, 2023
Closed
3 tasks
@mo271
Copy link
Copy Markdown
Collaborator Author

mo271 commented Sep 10, 2023 •
edited
Loading

see #6840 and discussion here:
#6806 (comment)

@mo271 mo271 marked this pull request as ready for review September 10, 2023 08:31
@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 13, 2023
jcommelin
jcommelin reviewed Sep 14, 2023
View reviewed changes
@jcommelin jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 14, 2023
@mo271 mo271 added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Sep 14, 2023
@mo271 mo271 added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Sep 14, 2023
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 14, 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 14, 2023
@bors bors bot changed the base branch from master to ScottCarnahan/BinomialRing2 September 17, 2023 03:26
@kim-em kim-em changed the base branch from ScottCarnahan/BinomialRing2 to master September 17, 2023 12:05
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Sep 19, 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 19, 2023
bors bot pushed a commit that referenced this pull request Sep 19, 2023
@mo271
chore: rm @simp from factorial (#7078)
fe39449 
Co-authored-by: Moritz Firsching <firsching@google.com>
@bors
Copy link
Copy Markdown

bors bot commented Sep 19, 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: rm @simp from factorial [Merged by Bors] - chore: rm @simp from factorial Sep 19, 2023
@bors bors bot closed this Sep 19, 2023
@bors bors bot deleted the mo271/no_simp_factorial branch September 19, 2023 16:22
kodyvajjha pushed a commit that referenced this pull request Sep 22, 2023
@mo271 @kodyvajjha
chore: rm @simp from factorial (#7078)
7f9b2e2 
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 left review comments

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.

2 participants

@mo271 @jcommelin