From 8220bb14e01b03ed727e8bb8c4f9ab70af3fd9f5 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sun, 14 Feb 2021 22:01:47 -0800
Subject: Show "Error:"/"Warning:" with white type (on red/orange background)

---
 doc/tools/coqrst/repl/ansicolors.py | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'doc/tools')

diff --git a/doc/tools/coqrst/repl/ansicolors.py b/doc/tools/coqrst/repl/ansicolors.py
index 9e23be2409..6700c20b1a 100644
--- a/doc/tools/coqrst/repl/ansicolors.py
+++ b/doc/tools/coqrst/repl/ansicolors.py
@@ -91,7 +91,10 @@ def parse_ansi(code):
                  leading ‘^[[’ or the final ‘m’
     """
     classes = []
-    parse_style([int(c) for c in code.split(';')], 0, classes)
+    if code == "37":
+        pass # ignore white fg
+    else:
+        parse_style([int(c) for c in code.split(';')], 0, classes)
     return ["ansi-" + cls for cls in classes]
 
 if __name__ == '__main__':
-- 
cgit v1.2.3