Skip to content

Conversation

@fingolfin
Copy link
Member

@fingolfin fingolfin added do not merge PRs which are not yet ready to be merged (e.g. submitted for discussion, or test results) release notes: not needed PRs introducing changes that are wholly irrelevant to the release notes topic: infrastructure topic: ci Anything related to GitHub Actions, Codecov, AppVeyor, Coveralls, Travis, ... and removed do not merge PRs which are not yet ready to be merged (e.g. submitted for discussion, or test results) labels Jan 26, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

release notes: not needed PRs introducing changes that are wholly irrelevant to the release notes topic: ci Anything related to GitHub Actions, Codecov, AppVeyor, Coveralls, Travis, ... topic: infrastructure

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant