From 7cedd02b5dbd2b23f126640307b95362d577cadf Mon Sep 17 00:00:00 2001 From: Peter Hutterer Date: Thu, 5 Jun 2014 15:42:49 +1000 Subject: [PATCH] tools: add a script to push the doxygen output to freedesktop.org Intentionally not added to EXTRA_DIST, if you're not running libinput from git you're not supposed to push documentation. Signed-off-by: Peter Hutterer --- tools/publish-doc | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100755 tools/publish-doc diff --git a/tools/publish-doc b/tools/publish-doc new file mode 100755 index 0000000..1e07e04 --- /dev/null +++ b/tools/publish-doc @@ -0,0 +1,11 @@ +#!/bin/bash + +set -e + +[ -e doc ] || echo "Run this from the project root" && exit 1 + +make + +[ -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.7.4