diff options
| -rw-r--r-- | doc/sphinx/_static/notations.css | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css index f899945a35..dcb47d1786 100644 --- a/doc/sphinx/_static/notations.css +++ b/doc/sphinx/_static/notations.css @@ -60,9 +60,10 @@ margin-right: 0.4em; /* Space for the right half of the sub- and sup-scripts */ } -.notation .hole { +.notation .hole, .std-token .pre { color: #4e9a06; font-style: italic; + font-weight: bold; } /***********************/ |