diff --git a/tools/publish-doc b/tools/publish-doc index 1e07e040..aa4b7412 100755 --- a/tools/publish-doc +++ b/tools/publish-doc @@ -2,10 +2,10 @@ set -e -[ -e doc ] || echo "Run this from the project root" && exit 1 +[ -e doc ] || (echo "Run this from the project root" && exit 1) make -[ -e doc/html ] || echo "HTML documentation failed to build" && exit 1 +[ -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