Skip to content

dev-docs: start collecting CI errors#2016

Merged
katexochen merged 1 commit intomainfrom
p/ci-errors
Dec 9, 2025
Merged

dev-docs: start collecting CI errors#2016
katexochen merged 1 commit intomainfrom
p/ci-errors

Conversation

@katexochen
Copy link
Member

No description provided.

@katexochen katexochen added the no changelog PRs not listed in the release notes label Dec 8, 2025
@katexochen katexochen requested a review from charludo December 8, 2025 09:30
Copy link
Collaborator

@charludo charludo left a comment

Choose a reason for hiding this comment

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

Helpful indeed!
Probably easiest to just add an exclude on the file in treefmt.nix?

@katexochen katexochen merged commit 2aa6be7 into main Dec 9, 2025
10 of 15 checks passed
@katexochen katexochen deleted the p/ci-errors branch December 9, 2025 12:54
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

no changelog PRs not listed in the release notes

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants