From c9ecf037ecd2e5ab84294d955a344ccf981e17b0 Mon Sep 17 00:00:00 2001 From: Stefan Frijters Date: Fri, 4 Jun 2021 15:03:41 +0200 Subject: 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`. --- doc/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/Makefile b/doc/Makefile index 7affbb0bb51..4308da148be 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 -- cgit 1.4.1