Do not include man pages in help

milasudril · Mar 2, 2021 · a7c6448 · a7c6448
1 parent b785339
commit a7c6448
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/devtools/make_doc_page.py b/devtools/make_doc_page.py
@@ -39,7 +39,7 @@ def get_title_dir(dir):
 class Entry:
 	def __init__(self, path):
 		if (path.name == 'index.md' or path.name == 'README.md' or path.name == '.git'
-			or path.name.startswith('__')):
+			or path.name.startswith('__') or path.name.endswith('.man.md')):
 			self.page = None
 			self.title = None
 			self.children = []