Toggle editor buttons when jumping to a source line

2021-12-21 13:26:06 +01:00
parent 0f92e862c6
commit 3dc8265292
1 changed files with 1 additions and 0 deletions
--- a/app/assets/javascripts/editor/editor.js.erb
+++ b/app/assets/javascripts/editor/editor.js.erb
@ -631,6 +631,7 @@ var CodeOceanEditor = {

        const frame = $('div.frame[data-filename="' + file + '"]');
        this.showFrame(frame);
+        this.toggleButtonStates();

        const file_id = frame.find('.editor').data('file-id');
        this.setActiveFile(frame.data('filename'), file_id);