Remove publish-doc

We don't use this script anymore.

Signed-off-by: Simon Ser <contact@emersion.fr>
This commit is contained in:
Simon Ser 2022-05-05 11:24:11 +02:00
parent 1078ee4993
commit 04efea1727

View file

@ -1,15 +0,0 @@
#!/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/