From f07cad4da54e63408cbb76d8ceb2b0b769922dea Mon Sep 17 00:00:00 2001
From: Sebastian Serth <Sebastian.Serth@hpi.de>
Date: Sun, 2 Feb 2020 12:36:20 +0100
Subject: [PATCH] Disable reset active file for user defined files

---
 app/assets/javascripts/editor/editor.js.erb | 1 +
 1 file changed, 1 insertion(+)

diff --git a/app/assets/javascripts/editor/editor.js.erb b/app/assets/javascripts/editor/editor.js.erb
index 7eb8962e..417faa3b 100644
--- a/app/assets/javascripts/editor/editor.js.erb
+++ b/app/assets/javascripts/editor/editor.js.erb
@@ -488,6 +488,7 @@ configureEditors: function () {
 
   toggleButtonStates: function () {
     $('#destroy-file').prop('disabled', this.active_frame.data('role') !== 'user_defined_file');
+    $('#start-over-active-file').prop('disabled', this.active_frame.data('role') === 'user_defined_file');
     $('#dummy').toggle(!this.fileActionsAvailable());
     $('#render').toggle(this.isActiveFileRenderable());
     $('#run').toggle(this.isActiveFileRunnable() && !this.running);