File tree 1 file changed +8
-1
lines changed
1 file changed +8
-1
lines changed Original file line number Diff line number Diff line change @@ -103,6 +103,13 @@ jobs:
103
103
echo "Tag ${TAG_NAME} did not match SemVer regex."
104
104
fi
105
105
106
+ - name : Check for custom releases (e.g., not in the main lean repository)
107
+ if : startsWith(github.ref, 'refs/tags/') && github.repository != 'leanprover/lean4'
108
+ id : set-release-custom
109
+ run : |
110
+ TAG_NAME="${GITHUB_REF##*/}"
111
+ echo "RELEASE_TAG=$TAG_NAME" >> "$GITHUB_OUTPUT"
112
+
106
113
- name : Set check level
107
114
id : set-level
108
115
# We do not use github.event.pull_request.labels.*.name here because
@@ -111,7 +118,7 @@ jobs:
111
118
run : |
112
119
check_level=0
113
120
114
- if [[ -n "${{ steps.set-nightly.outputs.nightly }}" || -n "${{ steps.set-release.outputs.RELEASE_TAG }}" ]]; then
121
+ if [[ -n "${{ steps.set-nightly.outputs.nightly }}" || -n "${{ steps.set-release.outputs.RELEASE_TAG }}" || -n "${{ steps.set-release-custom.outputs.RELEASE_TAG }}" ]]; then
115
122
check_level=2
116
123
elif [[ "${{ github.event_name }}" != "pull_request" ]]; then
117
124
check_level=1
You can’t perform that action at this time.
0 commit comments