v0.11.0 polish: the Debug Build message, the release badge on tags, the CI timings #56

Merged
twisla merged 3 commits from fix-release-polish into main 2026-10-06 15:21:43 +00:00
Showing only changes of commit 12006bdf94 - Show all commits
+3 -2
View File
@@ -59,9 +59,10 @@ jobs:
if: github.event_name == 'pull_request' || github.ref_type == 'tag' if: github.event_name == 'pull_request' || github.ref_type == 'tag'
run: scripts/ci.sh builds run: scripts/ci.sh builds
# The README's badges are files on a branch of their own, replaced at each push to main. # The README's badges are files on a branch of their own, replaced at each push to main and
# at each tag (the release badge says which tag is the latest)
- name: Publish the badges - name: Publish the badges
if: github.event_name == 'push' && github.ref == 'refs/heads/main' if: github.event_name == 'push' && (github.ref == 'refs/heads/main' || github.ref_type == 'tag')
env: env:
GITEA_TOKEN: ${{ secrets.GITEA_TOKEN }} GITEA_TOKEN: ${{ secrets.GITEA_TOKEN }}
run: | run: |