diff --git a/tools/publish-doc b/tools/publish-doc new file mode 100755 index 00000000..1e07e040 --- /dev/null +++ b/tools/publish-doc @@ -0,0 +1,11 @@ +#!/bin/bash + +set -e + +[ -e doc ] || echo "Run this from the project root" && exit 1 + +make + +[ -e doc/html ] || echo "HTML documentation failed to build" && exit 1 + +rsync --delete -avz doc/html/ freedesktop.org:/srv/wayland.freedesktop.org/www/libinput/doc/latest