File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -323,33 +323,6 @@ jobs:
323323 path : ${{ env.ARTEFACT }}.zip
324324 retention-days : 1
325325
326- # dev release (optional)
327- - name : 🚢 Create/Update Dev Release
328- if : (github.ref == 'refs/heads/dev' || github.ref == 'refs/heads/ci') && matrix.agda == 'Agda-2.8.0' && matrix.os == 'ubuntu-latest'
329- env :
330- GITHUB_TOKEN : ${{ secrets.GITHUB_TOKEN }}
331- run : |
332- # Delete existing dev release if it exists
333- gh release delete dev --cleanup-tag -y || true
334-
335- # Wait for GitHub to process the deletion to avoid race condition
336- # that causes releases to be created as drafts
337- # See: https://github.com/cli/cli/issues/8458
338- sleep 5
339-
340- # Create new dev pre-release
341- gh release create dev \
342- --title "Development Release (dev)" \
343- --notes "Development pre-release build from latest changes. This is a pre-release for testing purposes." \
344- --prerelease
345-
346- - name : 📤 Upload artifacts to dev release
347- if : (github.ref == 'refs/heads/dev' || github.ref == 'refs/heads/ci') && matrix.agda == 'Agda-2.8.0'
348- env :
349- GITHUB_TOKEN : ${{ secrets.GITHUB_TOKEN }}
350- run : |
351- gh release upload dev $ARTEFACT.zip --clobber
352-
353326 build-wasm :
354327 name : Build WASM
355328 if : github.ref == 'refs/heads/dev' || github.ref == 'refs/heads/ci'
You can’t perform that action at this time.
0 commit comments