Skip to content

Capitalize CI job names and rename gate job to merge_ready#175

Merged
djbender merged 1 commit intomainfrom
ci-job-names
Apr 12, 2026
Merged

Capitalize CI job names and rename gate job to merge_ready#175
djbender merged 1 commit intomainfrom
ci-job-names

Commits

Commits on Apr 12, 2026