[docs] move site gen to a post-push hook

This commit is contained in:
Jan Petykiewicz 2026-04-19 00:09:33 -07:00
commit 9453e9203a
4 changed files with 81 additions and 61 deletions

42
.githooks/post-push Executable file
View file

@ -0,0 +1,42 @@
#!/bin/bash
set -Eeuo pipefail
REMOTE_NAME="${1:-}"
REMOTE_URL="${2:-}"
if [[ "${MEANAS_DOCS_PUBLISHING:-0}" == "1" ]]; then
exit 0
fi
if [[ "$REMOTE_NAME" != "origin" ]]; then
exit 0
fi
publish_docs=0
while read -r local_ref local_sha remote_ref remote_sha; do
if [[ "$local_ref" == "refs/heads/master" && "$remote_ref" == "refs/heads/master" && "$local_sha" != "0000000000000000000000000000000000000000" ]]; then
publish_docs=1
break
fi
done
if [[ "$publish_docs" != "1" ]]; then
exit 0
fi
ROOT="$(git rev-parse --show-toplevel)"
cd "$ROOT"
if ! command -v mkdocs >/dev/null 2>&1; then
echo "[meanas docs hook] mkdocs not found; skipping docs publish" >&2
exit 0
fi
DOCS_SITE_URL="${DOCS_SITE_URL:-$(git config --get meanas.docsSiteUrl || true)}"
export DOCS_SITE_URL
echo "[meanas docs hook] building docs after push to ${REMOTE_NAME} (${REMOTE_URL})" >&2
MEANAS_DOCS_PUBLISHING=1 ./make_docs.sh
echo "[meanas docs hook] publishing docs-site branch" >&2
MEANAS_DOCS_PUBLISHING=1 ./scripts/publish_docs_branch.sh site docs-site