1 files changed, 12 insertions, 0 deletions
diff --git a/doc/utils/cleanhtml.sh b/doc/utils/cleanhtml.sh
new file mode 100755
index 000000000..a3ea2afac
--- /dev/null
+++ b/doc/utils/cleanhtml.sh
@@ -0,0 +1,12 @@
+# script to clean up HTML files
+# removes formatting added by htmldoc
+#
+# first argument is sedscript to use
+f=$1
+shift
+# remaining args are files to process
+for i
+do
+	sed -f $f $i > tmp
+	mv tmp $i
+done