diff options
| author | Jim Fehrle | 2021-02-10 22:56:31 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2021-04-17 09:41:42 -0700 |
| commit | e038e130188a0b43f66dfbc084cd8d9ca2cfb550 (patch) | |
| tree | b2d466d0c5ef6223ab86a0fb5abac0882cb09612 /doc/sphinx/_static | |
| parent | f337187f0ac4c2062031225234fd23b436b979b5 (diff) | |
Include (* ... *) comments in .. coqtop:: directives in Sphinx output
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 */ |