chiark / gitweb /
htmlman now deals with getting filenames right. Also quietens an