hub/script/publish-release

#!/usr/bin/env bash
set -e

publish_documentation() {
  local version="$1"
  local doc_dir="site"
  local doc_branch="gh-pages"

  git fetch origin "${doc_branch}:${doc_branch}"
  git worktree add "$doc_dir" "$doc_branch"
  pushd "$doc_dir"

  git rm hub*.html >/dev/null
  cp ../share/doc/*/*.html .

  git add hub*.html
  GIT_COMMITTER_NAME='GitHub Actions' GIT_COMMITTER_EMAIL='noreply@github.com' \
    GIT_AUTHOR_NAME='GitHub Actions' GIT_AUTHOR_EMAIL='noreply@github.com' \
    git commit -m "Update documentation for $version"

  git push origin HEAD
  popd
}

in_default_branch() {
  git fetch origin master --depth 10
  git merge-base --is-ancestor "$1" FETCH_HEAD
}

tag_name="${GITHUB_REF#refs/tags/}"
make man-pages
script/cross-compile "${tag_name#v}" | \
  PATH="bin:$PATH" script/github-release "$tag_name"

if [[ $tag_name != *-* ]] && in_default_branch "$tag_name"; then
  publish_documentation "$tag_name"
fi