# Keep the docs site's version badge in lockstep with releases. On every `v*` tag, rewrite the
# `.ghpill` badge in docs/index.html on `main` to the tag version and push — GitHub Pages then
# redeploys. Separate from the dist-generated release.yml (which is regenerated by `dist generate`).
#
# The push uses the default GITHUB_TOKEN, whose commits do NOT trigger further workflow runs, so
# there's no loop; `[skip ci]` is belt-and-suspenders.
name: docs version badge
on:
push:
tags:
permissions:
contents: write
jobs:
bump:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
with:
ref: main
- name: Rewrite the badge to the tag version
run: |
ver="${GITHUB_REF_NAME}" # e.g. v0.6.0
sed -i -E "s#(<span class=\"ghpill\">)v[0-9]+\.[0-9]+\.[0-9]+(</span>)#\1${ver}\2#" docs/index.html
if git diff --quiet -- docs/index.html; then
echo "version badge already ${ver} — nothing to do."
exit 0
fi
git config user.name codeshrew
git config user.email 155389+codeshrew@users.noreply.github.com
git add docs/index.html
git commit -m "docs: version badge → ${ver} [skip ci]"
git push origin main