From ad4011846909ddee59099e8d7554b95d9003257b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?S=C3=A9bastien=20Helleu?= <flashcode@flashtux.org>
Date: Sat, 25 May 2019 16:10:23 +0200
Subject: [PATCH] doc: increase font size for key bindings

---
 doc/docinfo.html | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/doc/docinfo.html b/doc/docinfo.html
index 8fae0da2b..88498d965 100644
--- a/doc/docinfo.html
+++ b/doc/docinfo.html
@@ -19,11 +19,12 @@ h1,h2,h3,h4,h5 {
   line-height: normal;
   font-size: .95em;
 }
-.keyseq kbd {
-  font-size: .7em;
+kbd {
+  font-size: .9em;
 }
 .tableblock kbd {
-  font-size: .7438em;
+  margin-top: .2em;
+  margin-bottom: .2em;
 }
 .hex {
   padding: 0 .2em;