docs: remove margin around logo background.

amaranth-lang · Apr 11, 2024 · c2ed5bf · c2ed5bf
1 parent 323122b
commit c2ed5bf
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/docs/_static/custom.css b/docs/_static/custom.css
@@ -11,7 +11,7 @@ a { text-decoration: underline; }
 /* Some of our section titles are looong */
 @media screen and (min-width:769px) {
   .wy-nav-side, .wy-side-scroll, .wy-menu-vertical { width: 340px; }
-  .wy-side-nav-search { width: 325px; }
+  .wy-side-nav-search { width: 340px; margin-bottom: .0em; }
   .wy-nav-content-wrap { margin-left: 340px; }
 }