From 6fa0c9aa975a1cd1fa1a122bf160380cd00b9de2 Mon Sep 17 00:00:00 2001 From: Peter Hutterer Date: Fri, 13 Jun 2014 14:43:28 +1000 Subject: [PATCH] tools: fix the publish-doc script Original script was broken, curse those last-minute changes before pushing Signed-off-by: Peter Hutterer --- tools/publish-doc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 -- 2.34.1