From aa2d687a15ed7f2e9bc5e09a350bf93993f4a4fe Mon Sep 17 00:00:00 2001
From: jous <git@jous.dudmail.com>
Date: Wed, 9 Jan 2013 01:47:30 +0200
Subject: [PATCH] removed unnecessary line

---
 js/functions.js | 1 -
 1 file changed, 1 deletion(-)

diff --git a/js/functions.js b/js/functions.js
index f1d5588b74..f386cbc434 100644
--- a/js/functions.js
+++ b/js/functions.js
@@ -3386,7 +3386,6 @@ AJAX.registerOnload('functions.js', function() {
             // ctrl-enter is 10 in chrome and ie, but 13 in ff
             if (e.ctrlKey && (e.keyCode == 13 || e.keyCode == 10)) { 
                 $("#button_submit_query").submit();
-                return false;
             }
         });
         codemirror_editor.focus();