max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: CI: allow releases not starting with v

Browse source
This commit is contained in:
Gabriel Ebner 2022-11-23 10:07:13 -08:00
parent 9b572d4e20
commit 06dc85453e
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
.github/workflows/ci.yml vendored
View file

@ -185,7 +185,7 @@ jobs:
dir=$(echo lean-*)
mkdir pack
# high-compression tar.zst + zip for release, fast tar.zst otherwise
if [[ '${{ startsWith(github.ref, 'refs/tags/v') && matrix.release }}' == true || -n '${{ needs.set-nightly.outputs.nightly }}' ]]; then
if [[ '${{ startsWith(github.ref, 'refs/tags/') && matrix.release }}' == true || -n '${{ needs.set-nightly.outputs.nightly }}' ]]; then
${{ matrix.tar || 'tar' }} cf - $dir | zstd -T0 --no-progress -19 -o pack/$dir.tar.zst
zip -rq pack/$dir.zip $dir
else
@ -235,7 +235,7 @@ jobs:
run: ccache -s
release:
if: startsWith(github.ref, 'refs/tags/v')
if: startsWith(github.ref, 'refs/tags/')
runs-on: ubuntu-latest
needs: build
steps: