From babf80b5abe6177bc250b08c0f455a86bb4cf973 Mon Sep 17 00:00:00 2001
From: Christophe HENRY <christophe.henry@sbgodin.fr>
Date: Mon, 1 Aug 2022 16:11:36 +0200
Subject: [PATCH] Fixes a margin bug in terminal.css

---
 css/default/terminal.css | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/css/default/terminal.css b/css/default/terminal.css
index 24e19b7..e45cd27 100644
--- a/css/default/terminal.css
+++ b/css/default/terminal.css
@@ -29,6 +29,14 @@ pre {
     padding: 1rem;
 }
 
+.menu a {
+    margin: 0;
+}
+
+.menu a:before {
+    content: "";
+}
+
 a {
     margin: -1.35rem;
     color: #090;