diff options
| author | coqbot-app[bot] | 2021-04-10 17:42:13 +0000 |
|---|---|---|
| committer | GitHub | 2021-04-10 17:42:13 +0000 |
| commit | 19e991811dc30bd2392cc969667887a159f355e5 (patch) | |
| tree | 16ba187adcaa3fceeb38b5f60a9c59b76424eb72 /doc/tools | |
| parent | 1947e54a2331dbbb8cd0f46b40bbb1524a67df54 (diff) | |
| parent | 8220bb14e01b03ed727e8bb8c4f9ab70af3fd9f5 (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/tools')
| -rw-r--r-- | doc/tools/coqrst/repl/ansicolors.py | 5 |
1 files changed, 4 insertions, 1 deletions
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__': |