diff options
author | Peter Hutterer <peter.hutterer@who-t.net> | 2014-06-13 14:43:28 +1000 |
---|---|---|
committer | Peter Hutterer <peter.hutterer@who-t.net> | 2014-06-16 16:44:34 +1000 |
commit | 6fa0c9aa975a1cd1fa1a122bf160380cd00b9de2 (patch) | |
tree | 08c690493e5ed1ea1bdaa0b79c6fdfe2399b4781 /tools | |
parent | 2e289b20266df9f0e2558366404aaf2833962fca (diff) | |
download | libinput-6fa0c9aa975a1cd1fa1a122bf160380cd00b9de2.tar.gz |
tools: fix the publish-doc script
Original script was broken, curse those last-minute changes before pushing
Signed-off-by: Peter Hutterer <peter.hutterer@who-t.net>
Diffstat (limited to 'tools')
-rwxr-xr-x | tools/publish-doc | 4 |
1 files 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 |