hub/script/publish-release

42 строки
1.1 KiB
Bash
Executable File

#!/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 .
local tracking="$(sed -n '/googletagmanager/,/^<\/script/p' index.html)"
local man_page
for man_page in hub*.html; do cat <<<"$tracking" >>"$man_page"; done
git add hub*.html
GIT_COMMITTER_NAME='GitHub Actions' GIT_COMMITTER_EMAIL='mislav+actions@github.com' \
GIT_AUTHOR_NAME='Mislav Marohnić' GIT_AUTHOR_EMAIL='mislav@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