Added script to deploy documentation to the web server

#!/bin/bash

OUTPUTDIR=./html

SSH_USER=tnl-doc

SSH_HOST=mmg-gitlab.fjfi.cvut.cz

SSH_PORT=22

SSH_TARGET_DIR=/srv/http/doc/tnl

set -e

# Run from this directory

cd ${0%/*}

[[ ! -d "$OUTPUTDIR" ]] && ./build

rsync -e "ssh -p $SSH_PORT" -P -rvzc --cvs-exclude --delete "$OUTPUTDIR/" "$SSH_USER@$SSH_HOST:$SSH_TARGET_DIR"