docs: Provide published branch

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

diff --git a/Makefile b/Makefile
index 5c256b66e0e056682653ad37af5fd6bb09b71796..952089a9dd3475660130a5ce17dbe27159538bbb 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -63,6 +63,7 @@ DEPLOY_ARCH=x86_64-unknown-linux-musl
 DEPLOY_RELEASE=debug
 DEPLOY_TARGET_DIR=$(TARGET_DIR)/$(addsuffix /,$(DEPLOY_ARCH))$(DEPLOY_RELEASE)
 DEPLOYED_BRANCH=deployed
+PUBLISHED_BRANCH=published
 
 #---------- nailing-cargo ----------
 
@@ -360,6 +361,7 @@ PUBLISH_DOC_SPHINX=$(PUBLISH_USER):public-html/otter/docs
 
 publish: doc-sphinx
        rsync -r --delete-delay docs/html/. $(PUBLISH_DOC_SPHINX)/.
+       git branch -f $(PUBLISHED_BRANCH)
 
 #---------- deployment ----------