Documentation fixes

+ Rename some txt2tags file from .txt to .t2t and remove abandoned .txt files.
+ Add program update_html that finds all .t2t documents and updates the
  corresponding .html file. It can be invoked with 'make html'.
+ Add style to some .html documents

1 files changed, 11 insertions, 0 deletions

diff --git a/bin/update_html b/bin/update_html
new file mode 100644
index 000000000..75f54b13e
--- /dev/null
+++ b/bin/update_html
@@ -0,0 +1,11 @@
+#!/bin/bash
+
+### This script finds all .t2t (txt2tags) files and updates the corresponding
+### .html file, if it is out-of-date.
+
+find . -name '*.t2t' | while read t2t ; do
+  html="${t2t%.t2t}.html"
+  if [ "$t2t" -nt "$html" ] ; then
+    txt2tags -thtml "$t2t"
+  fi
+done
\ No newline at end of file