Merge pull request #1073 from ninja-build/manual-font
authorNico Weber <nicolasweber@gmx.de>
Tue, 29 Dec 2015 15:08:42 +0000 (10:08 -0500)
committerNico Weber <nicolasweber@gmx.de>
Tue, 29 Dec 2015 15:08:42 +0000 (10:08 -0500)
use the default font size for manual headings


Trivial merge