From bc76d7ec438f742dd5beaa5ff6dd9cd978d57dcf Mon Sep 17 00:00:00 2001
From: Gareth Rees <gdr@garethrees.org>
Date: Tue, 25 Aug 2020 12:06:44 +0100
Subject: [PATCH] Correct background colour for code elements in the manual.

---
 mps/manual/source/themes/mps/static/mps.css_t | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/mps/manual/source/themes/mps/static/mps.css_t b/mps/manual/source/themes/mps/static/mps.css_t
index 5904c165580..882feba0772 100644
--- a/mps/manual/source/themes/mps/static/mps.css_t
+++ b/mps/manual/source/themes/mps/static/mps.css_t
@@ -152,7 +152,7 @@ pre, tt, code, a.mpstag {
     font-size: 100%;
 }
 
-.note tt, .warning tt, tt {
+tt, code {
     background: transparent;
 }
 
@@ -220,6 +220,14 @@ li.toctree-l1, li.toctree-l2, li.toctree-l3 {
     padding-top: 0 !important;
 }
 
+/* Override background-color for code elements. */
+.sphinxsidebar code {
+    background-color: {{ theme_sidebarbgcolor }};
+}
+.note code, .admonition code {
+    background-color: {{ theme_codebgcolor }};
+}
+
 /* Format the glossary index in two columns. */
 
 div#memory-management-glossary div#all {