docs: Provide publish target

Signed-off-by: Ian Jackson <ijackson@chiark.greenend.org.uk>

diff --git a/Makefile b/Makefile
index f4bf5d48f1a48613a9333143bf7bfe1da95cf942..5c256b66e0e056682653ad37af5fd6bb09b71796 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -353,6 +353,14 @@ stamp/wdt-%.lcheck:        $(WDT_DEPS)
        $(WDT_RUN) --as-if=lwdt-$* --layout=Landscape
        $(stamp)
 
+#---------- docs publication ----------
+
+PUBLISH_USER=ianmdlvl@login.chiark.greenend.org.uk
+PUBLISH_DOC_SPHINX=$(PUBLISH_USER):public-html/otter/docs
+
+publish: doc-sphinx
+       rsync -r --delete-delay docs/html/. $(PUBLISH_DOC_SPHINX)/.
+
 #---------- deployment ----------
 
 DEPLOY_USER=ian@login.chiark.greenend.org.uk