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.

Sign up for GitHub

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

Jump to bottom

Run make lint and other simple jobs in GitHub Actions #6969

Merged
merged 2 commits into from
Dec 12, 2023
Merged

Run make lint and other simple jobs in GitHub Actions #6969

merged 2 commits into from
Dec 12, 2023

Commits on Dec 11, 2023

  1. Run make lint job in GitHub Actions 

    This is a ground-up rewrite of the "lint" job instead of porting it from
CircleCI. It will be much faster since it doesn't try to spin up a
Docker container and work through our various unnecessary caching
layers. It does literally the bare minimum to run lints.

The CircleCI lint job needs to remain for now because it's super
intertwined with everything else.
    @legoktm
    legoktm committed Dec 11, 2023
    Configuration menu
    Copy the full SHA
    f2f594d View commit details
    Browse the repository at this point in the history

Commits on Dec 12, 2023

  1. Migrate some simple jobs to GitHub Actions

    @legoktm
    legoktm committed Dec 12, 2023
    Configuration menu
    Copy the full SHA
    42ae3f3 View commit details
    Browse the repository at this point in the history