5eea8355ba
Fixes a workflow bug where the `check-level` was not always set correctly. Arguments to a `gh` call used to determine the `check_level` were accidentally outside of the relevant command substitution (`$(gh ...)`). ----- This can be observed in [these logs](https://github.com/leanprover/lean4/actions/runs/10859763037/job/30139540920), where the check level (shown first under "configure build matrix") is `2`, but the PR does not have the `release-ci` tag. As a "test", run the script for "set check level" printed in those logs (with some lines omitted): ``` check_level=0 labels="$(gh api repos/leanprover/lean4/pulls/5343) --jq '.labels'" if echo "$labels" | grep -q "release-ci"; then check_level=2 elif echo "$labels" | grep -q "merge-ci"; then check_level=1 fi echo "check_level=$check_level" ``` Note that this prints `check_level=2`, but changing `labels` to `labels="$(gh api repos/leanprover/lean4/pulls/5343 --jq '.labels')"` prints `check_level=0`. |
||
|---|---|---|
| .. | ||
| actionlint.yml | ||
| backport.yml | ||
| check-prelude.yml | ||
| check-stage0.yml | ||
| ci.yml | ||
| copyright-header.yml | ||
| jira.yml | ||
| labels-from-comments.yml | ||
| nix-ci.yml | ||
| pr-release.yml | ||
| pr-title.yml | ||
| restart-on-label.yml | ||
| stale.yml | ||
| update-stage0.yml | ||