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`.
This commit is contained in:
Stefan Frijters 2021-06-04 15:03:41 +02:00
parent f36a65f6e2
commit c9ecf037ec
No known key found for this signature in database
GPG key ID: 7619A6BC6E7DFA6F

View file

@ -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