From c19d5e1867ef179f118f164a3457cb5366cf4055 Mon Sep 17 00:00:00 2001 From: Bryce Harrington Date: Wed, 27 May 2015 15:34:20 -0700 Subject: [PATCH] publish-doc: Add script for publishing docs to the website Adapted from same-named script from libinput. --- publish-doc | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100755 publish-doc diff --git a/publish-doc b/publish-doc new file mode 100755 index 00000000..80fc22a0 --- /dev/null +++ b/publish-doc @@ -0,0 +1,15 @@ +#!/bin/bash + +set -e + +[ -e doc ] || (echo "Run this from the project root" && exit 1) + +make + +DOC_HTML=./doc/publican/Wayland/en-US/html/ + +[ -e "${DOC_HTML}" ] || (echo "HTML documentation failed to build at ${DOC_HTML}" && exit 1) + +chmod -R g+x ${DOC_HTML} + +rsync --delete -avz ${DOC_HTML} freedesktop.org:/srv/wayland.freedesktop.org/www/docs/html/