Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - chore(analysis/normed_space/basic): reorder the restrict_scalars definitions#13995

Closed
eric-wieser wants to merge 2 commits intomasterfrom
eric-wieser/tidy-normed_space-restrict_scalars
Closed

[Merged by Bors] - chore(analysis/normed_space/basic): reorder the restrict_scalars definitions#13995
eric-wieser wants to merge 2 commits intomasterfrom
eric-wieser/tidy-normed_space-restrict_scalars

Conversation

@eric-wieser
Copy link
Copy Markdown
Member

This also update the docstrings to make normed_space.restrict_scalars even scarier.

The instances here themselves haven't actually changed.


Open in Gitpod

This also update the docstrings to make `normed_space.restrict_scalars` even scarier.
@eric-wieser eric-wieser added the awaiting-review The author would like community review of the PR label May 6, 2022
@eric-wieser eric-wieser changed the title chore(analysis/normed_space/basic): reorder the definitions chore(analysis/normed_space/basic): reorder the restrict_scalars definitions May 6, 2022
@ocfnash
Copy link
Copy Markdown
Collaborator

ocfnash commented May 10, 2022

Thanks!

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 May 10, 2022
bors bot pushed a commit that referenced this pull request May 10, 2022
…finitions (#13995)

This also update the docstrings to make `normed_space.restrict_scalars` even scarier.

The instances here themselves haven't actually changed.
@bors
Copy link
Copy Markdown

bors bot commented May 10, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(analysis/normed_space/basic): reorder the restrict_scalars definitions [Merged by Bors] - chore(analysis/normed_space/basic): reorder the restrict_scalars definitions May 10, 2022
@bors bors bot closed this May 10, 2022
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

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

Development

Successfully merging this pull request may close these issues.

2 participants