1 files changed, 26 insertions, 0 deletions
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:])
+