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

Fix erroneous header info after recent merge #12746

Merged
merged 1 commit into from
Jul 21, 2023
Merged

Fix erroneous header info after recent merge #12746

merged 1 commit into from
Jul 21, 2023

Conversation

msujew
Copy link
Member

@msujew msujew commented Jul 21, 2023

What it does

Fixes an error in our linter CI that appeared after a recent PR merge #12354.

How to test

Lint CI is supposed to be green

Review checklist

Reminder for reviewers

@msujew msujew added the linting issues related to linting label Jul 21, 2023
vince-fugnitto
vince-fugnitto approved these changes Jul 21, 2023
View reviewed changes
Copy link
Member

@vince-fugnitto vince-fugnitto left a comment

Choose a reason for hiding this comment

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

LGTM 👍

@msujew msujew merged commit d07fe93 into master Jul 21, 2023
6 checks passed
@github-actions github-actions bot added this to the 1.40.0 milestone Jul 21, 2023
@kittaakos
Copy link
Contributor

Thank you

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@vince-fugnitto vince-fugnitto vince-fugnitto approved these changes

Assignees
No one assigned
Labels
linting issues related to linting
Projects
PR Backlog
Archived in project
Milestone
1.40.0
Development

Successfully merging this pull request may close these issues.
3 participants
@msujew @kittaakos @vince-fugnitto