Skip to content

[Merged by Bors] - style: remove all easy leading bys#13419

Closed
grunweg wants to merge 3 commits intomasterfrom
MR-remove-leading-by
Closed

[Merged by Bors] - style: remove all easy leading bys#13419
grunweg wants to merge 3 commits intomasterfrom
MR-remove-leading-by

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented May 31, 2024

If a line starts with by , the previous line ends with := and the previous line is short enough,
move the "by " to the previous line to match the style guide.


The first commit was automatically generated using the auto-fix linter in #13420 (the commit is cherry-picked from this PR).
The second commit are some manual adjustments: I'm happy to drop them.


Open in Gitpod

@grunweg grunweg force-pushed the MR-remove-leading-by branch from 1d3f643 to 3d52e51 Compare May 31, 2024 17:37
Copy link
Copy Markdown
Contributor

@Ruben-VandeVelde Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

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

maintainer merge

@github-actions
Copy link
Copy Markdown

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label May 31, 2024
Copy link
Copy Markdown
Member

@jcommelin jcommelin 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 merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 1, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 1, 2024
If a line starts with `by `, the previous line ends with `:=` and the previous line is short enough,
move the "by " to the previous line to match the style guide.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 1, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title style: remove all easy leading bys [Merged by Bors] - style: remove all easy leading bys Jun 1, 2024
@mathlib-bors mathlib-bors bot closed this Jun 1, 2024
@mathlib-bors mathlib-bors bot deleted the MR-remove-leading-by branch June 1, 2024 05:50
callesonne pushed a commit that referenced this pull request Jun 4, 2024
If a line starts with `by `, the previous line ends with `:=` and the previous line is short enough,
move the "by " to the previous line to match the style guide.
mathlib-bors bot pushed a commit that referenced this pull request Jun 8, 2024
Follow-up on #13419: fix three cases with an easy fix which were merged since then, and three harder cases.
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
If a line starts with `by `, the previous line ends with `:=` and the previous line is short enough,
move the "by " to the previous line to match the style guide.
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
Follow-up on #13419: fix three cases with an easy fix which were merged since then, and three harder cases.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants