mirror of
https://gitlab.freedesktop.org/libinput/libinput.git
synced 2025-12-25 11:40:06 +01:00
7cedd02b5d
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>
11 lines
262 B
Bash
Executable file
11 lines
262 B
Bash
Executable file
#!/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
|