gendocs.sh: default to a common CSS style sheet for HTML output * build-aux/gendocs.sh (htmlarg): Change default value.
2014-12-11T16:49:21