David Herrmann 724b030894 docs: fix default font-size=12 documentation
We used font-size=15 in the past but changed it long ago. However, the
documentation still used 15 so fix this now.

Reported-by: James Buren <ryu0@ymail.com>
Signed-off-by: David Herrmann <dh.herrmann@googlemail.com>
2012-12-21 14:13:00 +01:00
..