From 4f79a17c0d2e13a21b4f4b54899e4d4705d7a6b4 Mon Sep 17 00:00:00 2001
From: Egor Tensin <Egor.Tensin@gmail.com>
Date: Wed, 23 Mar 2022 10:14:40 +0300
Subject: shell: adjust for recent font size increase

---
 assets/css/jekyll-theme/shell.css | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/assets/css/jekyll-theme/shell.css b/assets/css/jekyll-theme/shell.css
index 6e8ddce..7494508 100644
--- a/assets/css/jekyll-theme/shell.css
+++ b/assets/css/jekyll-theme/shell.css
@@ -5,12 +5,12 @@
 }
 
 /* WTF is this? I somehow came up with it, but I hope there's a better way.
- * 10.5px is the standard bottom margin for <pre>s. */
+ * 11px is the standard bottom margin for <pre>s. */
 .shell {
-  margin-bottom: 10.5px;
+  margin-bottom: 11px;
 }
 .shell + .shell {
-  margin-top: -10.5px;
+  margin-top: -11px;
 }
 
 .shell > div {
-- 
cgit v1.2.3