Skip to content

[Merged by Bors] - chore: tidy various files#11490

Closed
Ruben-VandeVelde wants to merge 2 commits intomasterfrom
various-tidy
Closed

[Merged by Bors] - chore: tidy various files#11490
Ruben-VandeVelde wants to merge 2 commits intomasterfrom
various-tidy

Conversation

@Ruben-VandeVelde
Copy link
Copy Markdown
Contributor


Open in Gitpod

Copy link
Copy Markdown
Contributor

@sgouezel sgouezel left a comment

Choose a reason for hiding this comment

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

bors d+
Thanks!

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 19, 2024

✌️ Ruben-VandeVelde can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Mar 19, 2024
@Ruben-VandeVelde
Copy link
Copy Markdown
Contributor Author

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Mar 19, 2024
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 19, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: tidy various files [Merged by Bors] - chore: tidy various files Mar 19, 2024
@mathlib-bors mathlib-bors bot closed this Mar 19, 2024
@mathlib-bors mathlib-bors bot deleted the various-tidy branch March 19, 2024 21:20
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
utensil pushed a commit that referenced this pull request Mar 26, 2024
xgenereux pushed a commit that referenced this pull request Apr 15, 2024
atarnoam pushed a commit that referenced this pull request Apr 16, 2024
uniwuni pushed a commit that referenced this pull request Apr 19, 2024
callesonne pushed a commit that referenced this pull request Apr 22, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer).

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants