Skip to content

Add a dev-mode CI#2639

Merged
mshinwell merged 1 commit intomainfrom
nroberts/add-dev-ci
May 31, 2024
Merged

Add a dev-mode CI#2639
mshinwell merged 1 commit intomainfrom
nroberts/add-dev-ci

Conversation

@ncik-roberts
Copy link
Copy Markdown
Contributor

@ncik-roberts ncik-roberts commented May 30, 2024

Adds a CI action that builds the compiler and runs tests with --enable-dev.

This checks that a PR doesn't break our local build configuration.

@ncik-roberts ncik-roberts force-pushed the nroberts/add-dev-ci branch from 261e8a6 to 0556f4a Compare May 30, 2024 20:15
@ncik-roberts ncik-roberts marked this pull request as ready for review May 30, 2024 20:28
@ncik-roberts
Copy link
Copy Markdown
Contributor Author

This adds a new job that takes 7m 21s to run, which is less than any of the other build/run jobs, which are generally above 10m. This seems like a good use of a CI slot to me but I'll let @mshinwell weigh in.

@ncik-roberts ncik-roberts requested a review from mshinwell May 30, 2024 20:29
@ncik-roberts ncik-roberts added the CI Github Actions CI changes label May 30, 2024
@mshinwell mshinwell merged commit 22b7186 into main May 31, 2024
@mshinwell mshinwell deleted the nroberts/add-dev-ci branch May 31, 2024 15:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

CI Github Actions CI changes

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants