New file, tweak-html

diff --git a/doc/tweak-html b/doc/tweak-html
new file mode 100755 (executable)
index 0000000..44d208b
--- /dev/null
+++ b/doc/tweak-html
@@ -0,0 +1,6 @@
+#!/bin/sh
+
+# Tweak the HTML generated by pandoc into the form we want
+
+cat ${@+"$@"} |
+    sed '/^<col width="[0-9]*%" \/>$//d'