From 0032f7788af60177609e47174c1d3e9244168dc5 Mon Sep 17 00:00:00 2001 From: ChenXin Date: Fri, 16 Aug 2019 17:40:16 +0800 Subject: [PATCH] update docs-tools --- docs/Makefile | 2 +- docs/format.py | 5 ++++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/docs/Makefile b/docs/Makefile index b9f1cf95..b41beb44 100644 --- a/docs/Makefile +++ b/docs/Makefile @@ -20,7 +20,7 @@ server: cd build/html && python -m http.server dev: - rm -rf build/html && make html && make server + rm -rf build && make html && make server .PHONY: help Makefile diff --git a/docs/format.py b/docs/format.py index 7cc341c2..67671ae7 100644 --- a/docs/format.py +++ b/docs/format.py @@ -59,7 +59,10 @@ def clear(path='./source/'): else: shorten(path + file, to_delete) for file in to_delete: - os.remove(path + file + ".rst") + try: + os.remove(path + file + ".rst") + except: + pass clear()