From 7ef145cdc5f575ae253b6bd0176375feee61bf86 Mon Sep 17 00:00:00 2001
From: Daniel Thompson <daniel@redfelineninja.org.uk>
Date: Sat, 11 Apr 2020 20:49:52 +0100
Subject: [PATCH] docs: Makefile: Try to avoid nuking the .git directory...

... if there is one.
---
 docs/Makefile | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/docs/Makefile b/docs/Makefile
index ed88099..ea7a6c8 100644
--- a/docs/Makefile
+++ b/docs/Makefile
@@ -12,6 +12,13 @@ BUILDDIR      = build
 help:
 	@$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)
 
+clean:
+	-mv build/html/.git build.html.git
+	@$(SPHINXBUILD) -M clean "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)
+	mkdir -p build/html/
+	-mv build.html.git build/html/.git
+
+
 .PHONY: help Makefile
 
 # Catch-all target: route all unknown targets to Sphinx using the new