aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/_static
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-04-10 17:42:13 +0000
committerGitHub2021-04-10 17:42:13 +0000
commit19e991811dc30bd2392cc969667887a159f355e5 (patch)
tree16ba187adcaa3fceeb38b5f60a9c59b76424eb72 /doc/sphinx/_static
parent1947e54a2331dbbb8cd0f46b40bbb1524a67df54 (diff)
parent8220bb14e01b03ed727e8bb8c4f9ab70af3fd9f5 (diff)
Merge PR #13860: [coqrst] Show "Error:"/"Warning:" with white type (on red/orange background)
Reviewed-by: Zimmi48 Ack-by: cpitclaudel
Diffstat (limited to 'doc/sphinx/_static')
-rw-r--r--doc/sphinx/_static/ansi.css2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/_static/ansi.css b/doc/sphinx/_static/ansi.css
index 2a618f68d2..a4850a738b 100644
--- a/doc/sphinx/_static/ansi.css
+++ b/doc/sphinx/_static/ansi.css
@@ -69,7 +69,7 @@
}
.ansi-fg-white {
- color: #2e3436;
+ color: #ffffff;
}
.ansi-fg-light-black {