Add new file role teacher_defined_linter

2020-10-15 00:43:57 +02:00
parent a5416758eb
commit be3ec82bd4
17 changed files with 41 additions and 28 deletions
--- a/app/assets/javascripts/editor/editor.js.erb
+++ b/app/assets/javascripts/editor/editor.js.erb
@ -413,7 +413,7 @@ var CodeOceanEditor = {
    },

    isActiveFileTestable: function () {
-        return this.isActiveFileExecutable() && ['teacher_defined_test', 'user_defined_test'].includes(this.active_frame.data('role'));
+        return this.isActiveFileExecutable() && ['teacher_defined_test', 'user_defined_test', 'teacher_defined_linter'].includes(this.active_frame.data('role'));
    },

    isBrowserSupported: function () {