Skip to content

Commit 1c002d1

Browse files
committed
Remove more unused generated files from help
1 parent 184882d commit 1c002d1

File tree

1 file changed

+5
-1
lines changed

1 file changed

+5
-1
lines changed

createdocs.py

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@
99
# but not all the input. To build the docs you need to clone the git repo
1010

1111
import os
12+
import shutil
1213
import subprocess
1314

1415

@@ -36,6 +37,9 @@
3637
raise RuntimeError("Error generating docs: %d\nStderr\n%s\nStdout\n%s" %
3738
(result.returncode, result.stderr.decode('utf8'), result.stdout.decode('utf8')))
3839

39-
UNUSED_FILES = ["flexsearch.min.js", "mermaid.min.js"]
40+
UNUSED_DIRS = ["categories", "commands", "fonts", "katex", "tags", "stdlib"]
41+
UNUSED_FILES = ["404.html", "flexsearch.min.js", "mermaid.min.js", "sitemap.xml"]
42+
for unused_dir in UNUSED_DIRS:
43+
shutil.rmtree(os.path.join("help", unused_dir))
4044
for unused_file in UNUSED_FILES:
4145
os.remove(os.path.join("help", unused_file))

0 commit comments

Comments
 (0)