aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-12-03 09:35:09 +0000
committerGitHub2020-12-03 09:35:09 +0000
commita88568e751d63d8db93450213272c8b28928dbf2 (patch)
treeb014c3e4bc498c6d8d67ef58a4557b3adf540c45 /doc
parent11730fa0ed2cb10da1ffc00f4f1140572134937e (diff)
parentaf0276ffe32e5367bd93e2e16bc57eecb0cf9de5 (diff)
Merge PR #13554: Split long lines in errors and warning index
Reviewed-by: Zimmi48
Diffstat (limited to 'doc')
-rw-r--r--doc/sphinx/_static/notations.css10
1 files changed, 10 insertions, 0 deletions
diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css
index 8c3f7ac3c1..abb08d98cc 100644
--- a/doc/sphinx/_static/notations.css
+++ b/doc/sphinx/_static/notations.css
@@ -266,3 +266,13 @@ code span.error {
.rst-content tt.literal, .rst-content tt.literal, .rst-content code.literal {
color: inherit !important;
}
+
+/* make the error message index readable */
+.indextable code {
+ white-space: inherit; /* break long lines */
+}
+
+.indextable tr td + td {
+ padding-left: 2em; /* indent 2nd & subsequent lines */
+ text-indent: -2em;
+}