Skip to content

[Merged by Bors] - doc(AlgebraicGeometry/Scheme): turn some comments into doc comments#11907

Closed
grunweg wants to merge 2 commits intomasterfrom
MR-doc-alggeo
Closed

[Merged by Bors] - doc(AlgebraicGeometry/Scheme): turn some comments into doc comments#11907
grunweg wants to merge 2 commits intomasterfrom
MR-doc-alggeo

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented Apr 4, 2024

and tweak formatting of some doc comments

Extracted from #11905.

Open in Gitpod

@grunweg grunweg added documentation Improvements or additions to documentation awaiting-review t-algebraic-geometry Algebraic geometry labels Apr 4, 2024
@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 Apr 5, 2024
@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 Apr 5, 2024
@joelriou
Copy link
Copy Markdown
Contributor

joelriou commented Apr 5, 2024

Thanks for doing this!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Apr 5, 2024
mathlib-bors bot pushed a commit that referenced this pull request Apr 5, 2024
@grunweg
doc(AlgebraicGeometry/Scheme): turn some comments into doc comments (#…
1c351ac 
…11907)

and tweak formatting of some doc comments

Extracted from #11905.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 5, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title doc(AlgebraicGeometry/Scheme): turn some comments into doc comments [Merged by Bors] - doc(AlgebraicGeometry/Scheme): turn some comments into doc comments Apr 5, 2024
@mathlib-bors mathlib-bors bot closed this Apr 5, 2024
@mathlib-bors mathlib-bors bot deleted the MR-doc-alggeo branch April 5, 2024 13:39
xgenereux pushed a commit that referenced this pull request Apr 15, 2024
@grunweg @xgenereux
doc(AlgebraicGeometry/Scheme): turn some comments into doc comments (#…
261bbf6 
…11907)

and tweak formatting of some doc comments

Extracted from #11905.
atarnoam pushed a commit that referenced this pull request Apr 16, 2024
@grunweg @atarnoam
doc(AlgebraicGeometry/Scheme): turn some comments into doc comments (#…
5f86d5f 
…11907)

and tweak formatting of some doc comments

Extracted from #11905.
uniwuni pushed a commit that referenced this pull request Apr 19, 2024
@grunweg @uniwuni
doc(AlgebraicGeometry/Scheme): turn some comments into doc comments (#…
5c8eac5 
…11907)

and tweak formatting of some doc comments

Extracted from #11905.
callesonne pushed a commit that referenced this pull request Apr 22, 2024
@grunweg @callesonne
doc(AlgebraicGeometry/Scheme): turn some comments into doc comments (#…
b3e0ac6 
…11907)

and tweak formatting of some doc comments

Extracted from #11905.
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

documentation Improvements or additions to documentation ready-to-merge This PR has been sent to bors. t-algebraic-geometry Algebraic geometry

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@grunweg @joelriou