From 86e411ac978cdd397000fce56508cb608697d976 Mon Sep 17 00:00:00 2001
From: Nicolas SAVOIS <nicolas.savois@gmail.com>
Date: Fri, 2 Sep 2016 12:22:49 +0200
Subject: [PATCH] added shortcut to execute query when Ctrl+Enter is pressed

---
 EST/js/app/Plugin.js | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/EST/js/app/Plugin.js b/EST/js/app/Plugin.js
index b7f4b3e..3a0b375 100644
--- a/EST/js/app/Plugin.js
+++ b/EST/js/app/Plugin.js
@@ -56,6 +56,9 @@ function initCodeMirror(element) {
         extraKeys: {
             "Ctrl-Q": function(cm) {
                 cm.foldCode(cm.getCursor());
+            },
+            "Ctrl-Enter": function(cm) {
+                gs.execute(gs.es);
             }
         },
         foldGutter: true,