#!/usr/bin/env bash

set -e

# unset GIT_WORK_TREE

# Build new web documentation:
make build-gh-pages