diff --git a/compile_server/app/static/editors.js b/compile_server/app/static/editors.js index bbf893a..936c3e6 100644 --- a/compile_server/app/static/editors.js +++ b/compile_server/app/static/editors.js @@ -522,7 +522,14 @@ function fill_editor_from_contents(container, example_name, example_server, } if (container.attr("prove_button")){ - var check_button = $('