diff options
Diffstat (limited to 'doc/sphinx/_static')
| -rw-r--r-- | doc/sphinx/_static/notations.css | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css index abb08d98cc..e262a9305d 100644 --- a/doc/sphinx/_static/notations.css +++ b/doc/sphinx/_static/notations.css @@ -267,6 +267,11 @@ code span.error { color: inherit !important; } + +.coqdoc-comment { + color: #808080 !important +} + /* make the error message index readable */ .indextable code { white-space: inherit; /* break long lines */ |