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`.
commitc9ecf037ecd2e5ab84294d955a344ccf981e17b0
authorStefan Frijters <sfrijters@gmail.com>
dateFri 4 Jun 2021, 15:03 (5 years ago)
parentf36a65f
doc/Makefile+1−1
@@ -22,7 +22,7 @@ fix-misc-xml:
2222.PHONY: clean
2323clean:
2424 rm -f ${MD_TARGETS} doc-support/result .version manual-full.xml functions/library/locations.xml functions/library/generated
25− rm -rf ./out/ ./highlightjs
25+ rm -rf ./out/ ./highlightjs ./media
2626
2727.PHONY: validate
2828validate: manual-full.xml doc-support/result