Add script for building GitHub pages to branch

This commit is contained in:
Dietrich Epp 2022-04-07 23:24:34 -04:00
parent e5e7749d2e
commit c7147b2737
2 changed files with 50 additions and 0 deletions

1
.gitignore vendored
View File

@ -1,2 +1,3 @@
/.user.bazelrc
/bazel-*
/gh-pages

49
docs/push.sh Executable file
View File

@ -0,0 +1,49 @@
#!/bin/sh
# Build the site and push it to GitHub pages.
set -e
root=$(git rev-parse --show-toplevel)
cd "$root"
if ! command -v frum >/dev/null ; then
echo >&2 "Error: frum is not installed"
exit 1
fi
if ! git diff-index --quiet --cached HEAD -- docs ; then
echo >&2 "Error: uncommitted changes"
exit 1
fi
if ! git diff-files --quiet docs ; then
echo >&2 "Error: uncommitted changes"
exit 1
fi
branch=$(git symbolic-ref HEAD)
if test "$branch" != refs/heads/main ; then
echo >&2 "Error: branch is not main"
exit 1
fi
commit="$(git rev-parse HEAD)"
echo >&2 "Checking out gh-pages..."
if test -d gh-pages ; then
branch=$(git -C gh-pages symbolic-ref HEAD)
if test "$branch" != refs/heads/gh-pages ; then
echo >&2 "Error: gh-pages dir does not have gh-pages branch"
exit 1
fi
else
git worktree add gh-pages
fi
echo >&2 "Building site..."
(
cd docs
eval "$(sh -c 'frum init')"
bundle exec jekyll build --destination ../gh-pages
)
echo >&2 "Committing..."
cd gh-pages
git add .
git commit -m "Generated from commit ${commit}"