From 8fe3a1e9ce76b2b62a2437ab739b45c171f25bd0 Mon Sep 17 00:00:00 2001
From: Florian Bruhin <git@the-compiler.org>
Date: Wed, 19 Aug 2015 07:13:33 +0200
Subject: [PATCH] Regenerate docs.

---
 doc/help/settings.asciidoc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/help/settings.asciidoc b/doc/help/settings.asciidoc
index 114f06b30..ec84b7d3f 100644
--- a/doc/help/settings.asciidoc
+++ b/doc/help/settings.asciidoc
@@ -1941,7 +1941,7 @@ Default: +pass:[8pt ${_monospace}]+
 === hints
 Font used for the hints.
 
-Default: +pass:[bold 12px Monospace]+
+Default: +pass:[bold 13px Monospace]+
 
 [[fonts-debug-console]]
 === debug-console