Skip to content

[Merged by Bors] - chore: add a few missing codeblock fences to doc-strings#39245

Closed
grunweg wants to merge 1 commit into
leanprover-community:masterfrom
grunweg:docstring-codeblocks
Closed

[Merged by Bors] - chore: add a few missing codeblock fences to doc-strings#39245
grunweg wants to merge 1 commit into
leanprover-community:masterfrom
grunweg:docstring-codeblocks

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented May 12, 2026

Found by the linter in #27897, but I expect the move to Verso would also have discovered this.


Open in Gitpod

@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented May 12, 2026

@Vierkantor Here's an easy PR reformatting a few doc-strings to (presumably) also become more verso-compliant. Do you mind taking a look? Thanks!

@grunweg grunweg requested a review from Vierkantor May 12, 2026 10:47
@github-actions github-actions Bot added the t-algebraic-geometry Algebraic geometry label May 12, 2026
@github-actions
Copy link
Copy Markdown

PR summary 424dce2f30

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.


No changes to strong technical debt.
No changes to weak technical debt.

Copy link
Copy Markdown
Contributor

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

bors r+

@mathlib-triage mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label May 12, 2026
mathlib-bors Bot pushed a commit that referenced this pull request May 12, 2026
Found by the linter in #27897, but I expect the move to Verso would also have discovered this.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors Bot commented May 12, 2026

Build failed (retrying...):

mathlib-bors Bot pushed a commit that referenced this pull request May 12, 2026
Found by the linter in #27897, but I expect the move to Verso would also have discovered this.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors Bot commented May 12, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title chore: add a few missing codeblock fences to doc-strings [Merged by Bors] - chore: add a few missing codeblock fences to doc-strings May 12, 2026
@mathlib-bors mathlib-bors Bot closed this May 12, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors. t-algebraic-geometry Algebraic geometry

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants