Files
zrepl_patched/docs/publish.sh
T
Christian Schwarz 4f950bb60a docs: simplify build + zrepl.github.io publishing (#913)
This PR simplifies how we build and publish docs:

- **Publish from `master` branch, retire `stable` branch.** The `stable`
branch was a manual step in the release process and often out of date.
Docs are now built and published directly from `master`.
Release-specific docs are available in the `zrepl-noarch.tar` asset on
each GitHub release.

- **build dependencies**: use `uv` for dependency management

- **zrepl.github.io: retire multi-version docs**: before this PR we used
`sphinx-multiversion` to publish multiple docs versions to
`zrepl.github.io`. This was never worth the pain, so, this PR removes it
in order to simplify stuff. Old docs are available in the GitHub
releases, and the docs now have a version dropdown that links there for
a hand-curated set of versions.

- **GitHub pages repo checkout**: use HTTPS because that's what I use
these days for all things GitHub. Switch CircleCI to a fine-grained PAT.

Refs
- docs bug https://github.com/zrepl/zrepl/issues/895
  - links to config examples should work again after this PR

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
2026-02-05 23:49:26 +01:00

92 lines
2.0 KiB
Bash
Executable File

#!/bin/bash
set -euo pipefail
GHPAGESREPO="https://github.com/zrepl/zrepl.github.io.git"
SCRIPTDIR=$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )
PUBLICDIR="${SCRIPTDIR}/public_git"
ROOTDIR="${SCRIPTDIR}/.."
PUSH=false
DO_CLONE=false
NON_INTERACTIVE=false
while getopts "caPh" arg; do
case "$arg" in
"a") NON_INTERACTIVE=true ;;
"c") DO_CLONE=true ;;
"P") PUSH=true ;;
"h") echo "Usage: $0 [-c clone] [-a auto/non-interactive] [-P push]"; exit 0 ;;
*) echo "invalid option"; exit 1 ;;
esac
done
cd "$SCRIPTDIR"
# Clone or verify repo
if [ ! -d "$PUBLICDIR" ]; then
if $DO_CLONE; then
git clone "${GHPAGESREPO}" "${PUBLICDIR}"
else
echo "Run with -c to clone ${GHPAGESREPO}"
exit 1
fi
fi
if ! $NON_INTERACTIVE; then
echo -n "PRESS ENTER to confirm you committed and pushed docs changes to the zrepl repo"
read -r
fi
# Verify we're in the right repo
cd "$PUBLICDIR"
REMOTE_URL=$(git remote get-url origin)
if [[ "$REMOTE_URL" != *"zrepl.github.io"* ]]; then
echo "ERROR: ${PUBLICDIR} remote is '${REMOTE_URL}', expected zrepl.github.io repo"
exit 1
fi
# Reset public repo to latest
echo "Resetting GitHub pages repo to latest commit..."
git fetch origin
git reset --hard origin/master
# Clean everything
echo "Cleaning GitHub pages repo..."
git rm -rf . || true
# Build docs
echo "Building docs..."
cd "$ROOTDIR"
make docs
# Copy built docs to public repo
echo "Copying built docs..."
cp -r artifacts/docs/html/* "$PUBLICDIR/"
# Commit
cd "$PUBLICDIR"
cat > .gitignore <<EOF
**/.doctrees
EOF
git add .gitignore
git add -A
CURRENT_COMMIT=$(git -C "$ROOTDIR" rev-parse HEAD)
if [ "$(git -C "$ROOTDIR" status --porcelain)" != "" ]; then
CURRENT_COMMIT="${CURRENT_COMMIT}(dirty)"
fi
COMMIT_MSG="docs: $(date -u) - ${CURRENT_COMMIT}"
if [ "$(git status --porcelain)" != "" ]; then
git commit -m "$COMMIT_MSG"
else
echo "Nothing to commit"
fi
if $PUSH; then
echo "Pushing to GitHub pages repo..."
git push origin master
else
echo "Not pushing. Use -P to push."
fi