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>

diff --git a/tools/publish-doc b/tools/publish-doc
index 1e07e0406b87d5c12fb79900b7782099f70c60ed..aa4b74126b167b6fd149a77d0b53371df35c032d 100755 (executable)
--- 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