diff options
| -rw-r--r-- | Makefile | 1 | ||||
| -rw-r--r-- | doc/_ext/px_cleaner.py | 26 |
2 files changed, 27 insertions, 0 deletions
@@ -73,6 +73,7 @@ WEBHOME = c:/ned/web/stellated/pages/code/coverage px: $(SPHINXBUILD) -b px $(SPHINXOPTS) doc/_build/px rm doc/_build/px/search.px + python doc/_ext/px_cleaner.py doc/_build/px/*.px dochtml: $(SPHINXBUILD) -b html $(SPHINXOPTS) doc/_build/html diff --git a/doc/_ext/px_cleaner.py b/doc/_ext/px_cleaner.py new file mode 100644 index 00000000..a5c00ff3 --- /dev/null +++ b/doc/_ext/px_cleaner.py @@ -0,0 +1,26 @@ +"""Clean up .px files created by Sphinx.""" + +import sys + +def clean_px(fname): + """Clean a px file.""" + + f = open(fname) + try: + text = f.read() + finally: + f.close() + text = text.lstrip() + f = open(fname, "w") + try: + f.write(text) + finally: + f.close() + +def clean_px_files(fnames): + for fname in fnames: + clean_px(fname) + +if __name__ == '__main__': + clean_px_files(sys.argv[1:]) + |