diff --git a/src/web/css/editor.css b/src/web/css/editor.css index e7e85bf6..6cea932b 100644 --- a/src/web/css/editor.css +++ b/src/web/css/editor.css @@ -480,6 +480,10 @@ div.CodeMirror span.CodeMirror-nonmatchingbracket-region { cursor: pointer; } +div.repl-animation { + background-color: var(--background) !important; +} + div.trace { overflow-x: auto; padding-top: 1px; diff --git a/src/web/js/repl-ui.js b/src/web/js/repl-ui.js index ddcb7b55..9fdfc9b1 100644 --- a/src/web/js/repl-ui.js +++ b/src/web/js/repl-ui.js @@ -342,7 +342,7 @@ }); var currentZIndex = 15000; runtime.setParam("current-animation-port", function(dom, title, closeCallback) { - var animationDiv = $("