diff options
| author | Daniel Thompson <daniel@redfelineninja.org.uk> | 2020-04-11 19:49:52 (GMT) |
|---|---|---|
| committer | Daniel Thompson <daniel@redfelineninja.org.uk> | 2020-04-11 19:49:52 (GMT) |
| commit | 7ef145cdc5f575ae253b6bd0176375feee61bf86 (patch) | |
| tree | 5438dcdfbf1fde4d181bb6a2b6c653f686a085f8 | |
| parent | e165f13a9e35b808096e5fa843811ea7d0f79501 (diff) | |
docs: Makefile: Try to avoid nuking the .git directory...
... if there is one.
| -rw-r--r-- | docs/Makefile | 7 |
1 files changed, 7 insertions, 0 deletions
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 |