1 files changed, 1 insertions, 0 deletions
diff --git a/js/Misc/DEBUG.js b/js/Misc/DEBUG.js
index e24992a4..e16c4c3d 100644
--- a/js/Misc/DEBUG.js
+++ b/js/Misc/DEBUG.js
@@ -36,6 +36,7 @@ function DEBUG() {
                     break;
                 } else {
                     message([["Error in the instructions"],[lasterror()]]);
+                    throw "user error";
                 }
             } else {
                 var ok = false;