diff --git a/tools/publish-doc b/tools/publish-doc deleted file mode 100755 index 1a91e1a6..00000000 --- a/tools/publish-doc +++ /dev/null @@ -1,22 +0,0 @@ -#!/bin/bash - -set -e - -[ -e doc ] || (echo "Run this from the project root" && exit 1) - -if ! [ -f build/build.ninja ]; then - echo "Setting up meson in directory 'build'" - meson build -fi -ninja -C build - -[ -e build/html ] || (echo "HTML documentation failed to build" && exit 1) - -path=latest - -if [ -n "$1" ]; then - echo "Pushing to directory '$1'" - path="$1" -fi - -rsync --delete -avz build/html/ freedesktop.org:/srv/wayland.freedesktop.org/www/libinput/doc/$path