#!/usr/bin/env bash set -e # Build new web documentation: make build-gh-pages