Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - chore(algebra/euclidean_domain): docstrings #3816

Closed
wants to merge 2 commits into from
Closed

[Merged by Bors] - chore(algebra/euclidean_domain): docstrings #3816

wants to merge 2 commits into from

Conversation

ChrisHughes24
Copy link
Member

@ChrisHughes24 ChrisHughes24 added the awaiting-review The author would like community review of the PR label Aug 15, 2020
@fpvandoorn
Copy link
Member

fpvandoorn commented Aug 15, 2020 •
edited

I did some of this in #3752. Do you want to "merge" these changes? Or shall I accept the other PR, and you make whatever changes you want on top of that?

@semorrison semorrison added awaiting-author A reviewer has asked the author a question or requested changes blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. and removed awaiting-review The author would like community review of the PR labels Aug 16, 2020
@semorrison
Copy link
Collaborator

I've marked this as blocked by #3752.

@fpvandoorn
Copy link
Member

fpvandoorn commented Aug 16, 2020 •
edited

I think an easy option is just to merge the other PR (which I just did), and then you can expand the docstrings more, and change the type name.

Probably we want to replace \a by R in the whole file.

@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Aug 16, 2020
@semorrison semorrison removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Aug 17, 2020
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Aug 18, 2020
@ChrisHughes24
Copy link
Member Author

I overwrote the other docstrings, because I think mine are a but more detailed. I also replaced alpha with R everwhere

@ChrisHughes24 ChrisHughes24 added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Aug 18, 2020
@fpvandoorn
Copy link
Member

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Aug 18, 2020
bors bot pushed a commit that referenced this pull request Aug 18, 2020
@ChrisHughes24
chore(algebra/euclidean_domain): docstrings (#3816)
0854e83 
Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
@bors
Copy link

bors bot commented Aug 18, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(algebra/euclidean_domain): docstrings [Merged by Bors] - chore(algebra/euclidean_domain): docstrings Aug 18, 2020
@bors bors bot closed this Aug 18, 2020
@bors bors bot deleted the ChrisHughes24-patch-3 branch August 18, 2020 18:31
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@ChrisHughes24 @fpvandoorn @semorrison