Skip to content

Help getting https://github.com/python/mypy/pull/9881 merged #10931

Closed
@FuegoFro

Description

@FuegoFro

Hi! The PR at #9881 has been ready for a while, and I'd be grateful if it could be merged in (or given feedback as to what else needs to change). I'm sorry if this isn't the right way to use GitHub issues, but I'm a bit at a loss for how else to get eyes on the PR (have tried pinging it and using the Gitter chat). If there's a different way I should handle a situation like this is the future, please let me know 🙏 Thank you!

Metadata

Metadata

Assignees

No one assigned

    Labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions