From 682019a70be477a4f76473c9f1a567bbc9ef223a Mon Sep 17 00:00:00 2001 From: Shyue Ping Ong Date: Fri, 20 Oct 2023 13:42:04 -0700 Subject: [PATCH] Fix tasks.py. --- tasks.py | 1 + 1 file changed, 1 insertion(+) diff --git a/tasks.py b/tasks.py index c88e39daa0a..01f47dabea3 100644 --- a/tasks.py +++ b/tasks.py @@ -64,6 +64,7 @@ def make_doc(ctx): # with open(fn, "w") as f: # f.write("\n".join(preamble + lines)) ctx.run("rm -r markdown", warn=True) + ctx.run("rm -r html", warn=True) # ctx.run("cp ../README.md index.md") ctx.run("cp ../CHANGES.md CHANGES.md") ctx.run("rm -rf doctrees", warn=True)