Skip to content

ci(nightly-testing): guard the bump-branch steps when the nightly bump branch exists - #914

Open
jessealama wants to merge 1 commit into
leanprover:mainfrom
jessealama:ci/nightly-bump-guards
Open

jessealama wants to merge 1 commit into
leanprover:mainfrom
jessealama:ci/nightly-bump-guards

Conversation

@jessealama

@jessealama jessealama commented Sep 16, 2026

Copy link
Copy Markdown
Contributor

The "Exit if matching branch exists" step did exit 0, which only ends that step. Since a zero exit is a success, the job simply moved on and the subsequent steps ran. When no bump/v4.x.0 branch existed, the first of them threw, and the if: failure() Zulip warning could post a misleading message about a toolchain pattern mismatch, but the real reason was the non-existence of the proper branch.

This PR drops the no-op step and guards both fetch steps on the branch check, as other later step already are. Post a dedicated warning to Zulip when no bump/v4.x.0 branch is found, and only post the toolchain warning when the toolchain fetch step itself failed.

Also replace new Exception, which is a ReferenceError in JavaScript, with new Error. Exception doesn't exist in JS. So, curiously, running this code caused a different kind of exception to be thrown (a ReferenceError for referring to something that doesn't exist), which ended up killing the step as intended, but for the wrong reason.

…p branch exists

The "Exit if matching branch exists" step ran `exit 0`, which only ends that
step, so the two following github-script steps ran unguarded. If no
bump/v4.x.0 branch existed, the first of them threw and the `if: failure()`
Zulip warning posted a misleading message about a toolchain pattern mismatch.

Drop the no-op step and guard both fetch steps on the branch check, matching
every later step. Post a dedicated Zulip warning when no bump/v4.x.0 branch is
found, and only post the pattern-mismatch warning when the toolchain fetch step
itself failed. Also replace `new Exception`, which is a ReferenceError in
JavaScript, with `new Error`.
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