* Sometimes you really do need or want punctuation in a heading, but ideally without something else generating whitespace and other annoyances to go with it. * Trying a real decimal point instead. Signed-off-by: Ben McGinnes <ben@adversary.org>