From bdb5150669d5ac972d3d2b3c9cc2045e77dc9ad5 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Tue, 24 Dec 2019 22:30:31 -0800
Subject: Show doc notations in boldface

---
 doc/sphinx/_static/notations.css | 1 +
 1 file changed, 1 insertion(+)

(limited to 'doc/sphinx/_static/notations.css')

diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css
index d654479b07..3806ba6ee6 100644
--- a/doc/sphinx/_static/notations.css
+++ b/doc/sphinx/_static/notations.css
@@ -10,6 +10,7 @@
 .notation {
     /* font-family: "Ubuntu Mono", "Consolas", monospace; */
     white-space: pre-wrap;
+    font-weight: bold;
 }
 
 .notation .notation-sup {
-- 
cgit v1.2.3