:wrench: Do not build benchmark docs by default

diff --git a/docs.mk b/docs.mk
index 78813d480e58f60a5d9aed948da67df98d50506a..d2fc79e7b32b2e17b2ac3368e7c2cdff700a56e1 100644 (file)
--- a/docs.mk
+++ b/docs.mk
@@ -3,7 +3,7 @@ $(shell cp docs/config.mk.orig docs/config.mk)
 endif
 include docs/config.mk
 
-mdr_list = $(shell find docs -type f -name "*.mdr")
+mdr_list = (filter-out docs/09_Benchmarks.mdr, $(shell find docs -type f -name "*.mdr"))
 md_list  = $(mdr_list:.mdr=.md)
 
 _docserver_config       = bash help/doc-config.sh > mkdocs.yml