Method $detachEditorEventHandlers

src/ext/diff/split_diff_view.js:208–211

(editor)

    }

    $detachEditorEventHandlers(editor) {
        editor.off("mousewheel", this.onMouseWheel);
        editor.off("input", this.onInput);
    }
}