File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -2,8 +2,6 @@ name: Check toolchain file
22
33on :
44 pull_request :
5- branches :
6- - main
75 merge_group :
86
97jobs :
1816 - name : Check whether lean-toolchain contains nightly
1917 id : check-nightly
2018 run : |
21- if grep -q "nightly" lean-toolchain; then
22- echo "::error::The lean-toolchain file contains 'nightly', which is not allowed in PRs to main"
23- exit 1
24- else
19+ BASE="${{ github.base_ref || github.event.merge_group.base_ref }}"
20+ echo "Base ref: $BASE"
21+ if [ "$BASE" = "main" ] || [ "$BASE" = "refs/heads/main" ]; then
22+ if grep -q "nightly" lean-toolchain; then
23+ echo "::error::The lean-toolchain file contains 'nightly', which is not allowed in PRs to main"
24+ exit 1
25+ fi
2526 echo "Lean toolchain is valid for main branch - no 'nightly' found"
27+ else
28+ echo "Base branch '$BASE' is not main; nightly toolchains are allowed."
2629 fi
You can’t perform that action at this time.
0 commit comments