From 99cfb3463998e670673e8fd49525cca9e5e02edf Mon Sep 17 00:00:00 2001
From: "john.j.camilleri" <john.j.camilleri@chalmers.se>
Date: Thu, 25 Jul 2013 07:36:34 +0000
Subject: [PATCH] RGL Browser: now includes Syntax Editor tab!

---
 src/www/syntax-editor/editor_menu.js | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/www/syntax-editor/editor_menu.js b/src/www/syntax-editor/editor_menu.js
index 3ebecb836..13d43233a 100644
--- a/src/www/syntax-editor/editor_menu.js
+++ b/src/www/syntax-editor/editor_menu.js
@@ -11,6 +11,7 @@ function EditorMenu(editor,opts) {
         show_to_menu: true,
         show_random_button: true,
         show_import: true,
+        show_debug: false,
     }
 
     // Apply supplied options
@@ -92,7 +93,9 @@ function EditorMenu(editor,opts) {
         ]);
     }
 
-    appendChildren(t.container, [t.ui.debug_toggle]);
+    if (t.options.show_debug) {
+        appendChildren(t.container, [t.ui.debug_toggle]);
+    }
 
     /* --- Client state initialisation -------------------------------------- */
     this.editor = editor;