Skip to content

[Merged by Bors] - feat(lint_and_suggest_pr.yml): mention the "bot fix style" command in the reviewdog comments#16365

Closed
bryangingechen wants to merge 1 commit intomasterfrom
bgc-advertise-bot-fix-style
Closed

[Merged by Bors] - feat(lint_and_suggest_pr.yml): mention the "bot fix style" command in the reviewdog comments#16365
bryangingechen wants to merge 1 commit intomasterfrom
bgc-advertise-bot-fix-style

Conversation

@bryangingechen
Copy link
Copy Markdown
Contributor

Cf. Zulip


Open in Gitpod

@bryangingechen bryangingechen added the CI Modifies the continuous integration setup or other automation label Aug 31, 2024
@github-actions
Copy link
Copy Markdown

PR summary da0dde40cb

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
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

Copy link
Copy Markdown
Contributor

@grunweg grunweg left a comment

Choose a reason for hiding this comment

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

Looks reasonable, let's try this!
maintainer merge

@github-actions
Copy link
Copy Markdown

🚀 Pull request has been placed on the maintainer queue by grunweg.

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

urkud commented Aug 31, 2024

Thanks! 🎉
bors merge

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 31, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(lint_and_suggest_pr.yml): mention the "bot fix style" command in the reviewdog comments [Merged by Bors] - feat(lint_and_suggest_pr.yml): mention the "bot fix style" command in the reviewdog comments Aug 31, 2024
@mathlib-bors mathlib-bors bot closed this Aug 31, 2024
@mathlib-bors mathlib-bors bot deleted the bgc-advertise-bot-fix-style branch August 31, 2024 19:37
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

CI Modifies the continuous integration setup or other automation 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