Skip to content

Add CI for dev_scripts - #48

Merged
empwilli merged 3 commits into
mainfrom
empwilli/add_ci_for_dev_scripts
Nov 24, 2025
Merged

empwilli merged 3 commits into
mainfrom
empwilli/add_ci_for_dev_scripts

Conversation

@empwilli

Copy link
Copy Markdown
Contributor

The utilities in dev_scripts are central for the orchestration
of our code generation. As such care must be taken to ensure
code quality. Therefore, we add a CI for the dev_scripts.

@empwilli
empwilli merged commit 0339582 into main Nov 24, 2025
1 check passed
@empwilli
empwilli deleted the empwilli/add_ci_for_dev_scripts branch November 24, 2025 15:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant