From 92a4948666d677c00ebf5caec6b86acd547c8295 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?S=C3=A9bastien=20Helleu?= <flashcode@flashtux.org>
Date: Sun, 26 May 2019 14:52:00 +0200
Subject: [PATCH] doc: add extra left/right margins on key sequences

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

diff --git a/doc/docinfo.html b/doc/docinfo.html
index 88498d965..389394b46 100644
--- a/doc/docinfo.html
+++ b/doc/docinfo.html
@@ -22,6 +22,10 @@ h1,h2,h3,h4,h5 {
 kbd {
   font-size: .9em;
 }
+.keyseq {
+  margin-left: .2em;
+  margin-right: .2em;
+}
 .tableblock kbd {
   margin-top: .2em;
   margin-bottom: .2em;