Add dev.css override

This commit is contained in:
Max Hilbrunner
2021-07-11 13:01:16 +02:00
parent c8d7e0a4ee
commit 50edc681f9
2 changed files with 11 additions and 0 deletions
+8
View File
@@ -0,0 +1,8 @@
/**
* CSS tweaks that are only added outside ReadTheDocs (i.e. when built locally).
*/
/* Re-add default red boxes around Pygments errors */
.highlight .err {
border: 1px solid #FF0000;
}
+3
View File
@@ -191,6 +191,9 @@ html_css_files = [
"css/custom.css",
]
if not on_rtd:
html_css_files.append("css/dev.css")
html_js_files = [
"js/custom.js",
('https://cdn.jsdelivr.net/npm/docsearch.js@2/dist/cdn/docsearch.min.js', {'defer': 'defer'}),