diff --git a/_static/css/dev.css b/_static/css/dev.css new file mode 100644 index 000000000..87ad1d310 --- /dev/null +++ b/_static/css/dev.css @@ -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; +} diff --git a/conf.py b/conf.py index d3a6ccf35..cff79a7e3 100644 --- a/conf.py +++ b/conf.py @@ -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'}),