diff options
| author | Peter Hutterer <peter.hutterer@who-t.net> | 2014-06-05 15:42:49 +1000 |
|---|---|---|
| committer | Peter Hutterer <peter.hutterer@who-t.net> | 2014-06-10 08:28:07 +1000 |
| commit | 7cedd02b5dbd2b23f126640307b95362d577cadf (patch) | |
| tree | ed7469f64950eb047e11d0076327256071a46577 /tools | |
| parent | f533ef212e47a449256324cfd8c5ed78df57b5da (diff) | |
| download | libinput-7cedd02b5dbd2b23f126640307b95362d577cadf.tar.gz | |
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 <peter.hutterer@who-t.net>
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/publish-doc | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/tools/publish-doc b/tools/publish-doc new file mode 100755 index 00000000..1e07e040 --- /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 |