diff options
| author | Stefan Frijters <sfrijters@gmail.com> | 2021-06-04 15:03:41 +0200 |
|---|---|---|
| committer | Stefan Frijters <sfrijters@gmail.com> | 2021-06-04 15:03:46 +0200 |
| commit | c9ecf037ecd2e5ab84294d955a344ccf981e17b0 (patch) | |
| tree | a3dbd645f61b479a0c1ac3654ed4333f929ce54b /doc/Makefile | |
| parent | f36a65f6e2e9f3641f12c7d6e48a5ec4b5c5394b (diff) | |
doc: Clean up generated media directory
pandoc uses ./media to extract media files - add it to the list
of directories that need to be removed by `make clean`.
Diffstat (limited to 'doc/Makefile')
| -rw-r--r-- | doc/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/Makefile b/doc/Makefile index 7affbb0bb51c..4308da148be9 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -22,7 +22,7 @@ fix-misc-xml: .PHONY: clean clean: rm -f ${MD_TARGETS} doc-support/result .version manual-full.xml functions/library/locations.xml functions/library/generated - rm -rf ./out/ ./highlightjs + rm -rf ./out/ ./highlightjs ./media .PHONY: validate validate: manual-full.xml doc-support/result |