Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Change php-lint-summary to lint-summary #8942

Closed
wants to merge 1 commit into from
Closed

Change php-lint-summary to lint-summary #8942

wants to merge 1 commit into from

Conversation

GretaD
Copy link
Contributor

@GretaD GretaD commented Oct 10, 2023

@GretaD GretaD self-assigned this Oct 10, 2023
@GretaD
Copy link
Contributor Author

GretaD commented Oct 10, 2023

/backport to stable3.2

@GretaD
Copy link
Contributor Author

GretaD commented Oct 10, 2023

/backport to stable2.2

@ChristophWurst
Copy link
Member

bc74426 standardized the workflows so I would not revert the rename but adjust any branches older than that commit

@GretaD
Copy link
Contributor Author

GretaD commented Oct 10, 2023

close on behalf of #8943

@GretaD GretaD closed this Oct 10, 2023
@ChristophWurst ChristophWurst deleted the change/php-lint-sumary branch October 10, 2023 12:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ChristophWurst ChristophWurst Awaiting requested review from ChristophWurst

@miaulalala miaulalala Awaiting requested review from miaulalala

Assignees

@GretaD GretaD

Labels
3. to review backport-request
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@GretaD @ChristophWurst