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.

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

Add missing type annotation #12668

Merged
merged 1 commit into from
Dec 27, 2023
Merged

Conversation

petere
Copy link
Contributor

@petere petere commented Dec 25, 2023

I noticed during unrelated work that the lint/mypy check was failing on this, so I propose this fix.

@dcbaker dcbaker merged commit 4351f56 into mesonbuild:master Dec 27, 2023
30 checks passed
@petere
Copy link
Contributor Author

petere commented Dec 28, 2023

I don't see this commit in the master branch. Was this merged correctly?

@tristan957
Copy link
Contributor

Hmm this is very strange. The commit that GitHub thinks is this commit on the master branch is something completely different. Wanna just re-open a PR, and we can try this again?

@eli-schwartz
Copy link
Member

This is a fascinating GitHub bug... @dcbaker since GitHub thinks you clicked merge on this (but I can't even be sure of that at this point) do you recall if this succeeded at any time?

@petere
Copy link
Contributor Author

petere commented Dec 28, 2023

Wanna just re-open a PR, and we can try this again?

Ok, let's try that.

@petere
Copy link
Contributor Author

petere commented Dec 28, 2023

Actually, this was already committed independently as 8bc8f93. So it's all done, just GitHub being a bit confused.

@petere petere deleted the fix-type-annot branch December 28, 2023 20:00
@eli-schwartz
Copy link
Member

That's... definitely one way of resolving a cherry-pick by determining that the resulting patch would be empty.

@dcbaker
Copy link
Member

dcbaker commented Dec 28, 2023

I was confused since I thought I’d already fixed this, but convinced myself it was a second instance of the same issue. Very strange behavior from GitHub indeed

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants