#!/bin/bash -x
# Kill the existing target directory and built docs
rev=
# Create a new target directory with an empty git repo
prev=
# Add generated docs and a redirect page to our new repo
# Add the real github repo as a remote and force-push everything
# we just committed to our new repo locally to the gh-pages branch
# Kill the target directory and hence the local repo