Skip to content

Integrate new tooling into pull request CI #1240

@horazont

Description

@horazont

Summary

In order to reduce the manual load on the editor, it is important that steps run automatically as far as reasonably possible.

Work proposal

Create a CI workflow which, on pull requests runs the tools created in #1235, #1237, #1238, #1239 and sends diagnostics in a comment on the GitHub PR, adding labels and tagging either the author or the editor as appropriate.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Editor ToolingIssue relates to process/tooling

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions