From ac3759dcee80e29052ffe78859ecd40f75e38775 Mon Sep 17 00:00:00 2001
From: Dan Helfman <dan@luminotes.com>
Date: Fri, 30 Nov 2007 04:00:31 +0000
Subject: [PATCH] Ignoring ctrl key being released in IE 6 and 7.

---
 static/js/Editor.js | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/static/js/Editor.js b/static/js/Editor.js
index 124154f..58f53b6 100644
--- a/static/js/Editor.js
+++ b/static/js/Editor.js
@@ -282,7 +282,8 @@ Editor.prototype.key_released = function ( event ) {
 
   // if ctrl keys are released, bail
   var code = event.key().code;
-  if ( event.modifier().ctrl )
+  var CTRL = 17;
+  if ( event.modifier().ctrl || code == CTRL )
     return;
 
   signal( this, "state_changed", this );