From 04efea1727f243ac1d243cee40daad1692fe2f90 Mon Sep 17 00:00:00 2001 From: Simon Ser Date: Thu, 5 May 2022 11:24:11 +0200 Subject: [PATCH] Remove publish-doc We don't use this script anymore. Signed-off-by: Simon Ser --- publish-doc | 15 --------------- 1 file changed, 15 deletions(-) delete mode 100755 publish-doc diff --git a/publish-doc b/publish-doc deleted file mode 100755 index 80fc22a..0000000 --- a/publish-doc +++ /dev/null @@ -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/ -- 2.7.4