#!/bin/sh set +eux if [ "$(hostname -s)" = "freeside" ] then HOST="$HOME/" else HOST="freeside.wntrmute.net:" fi cd docs && doxygen && rsync -auv html/ ${HOST}sites/wntrmute-dev/wrmath/ cd sphinx && make html && rsync -auv _build/html/ ${HOST}sites/wntrmute-dev/sphinx/