From 0201e0c683174f18e98084f5a06154bb16b532ec Mon Sep 17 00:00:00 2001
From: Trevor Elliott <trevor@galois.com>
Date: Wed, 31 Jul 2013 15:18:48 -0700
Subject: Remove some debug text

---
 src/js/fiveui/injected/ui.js | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/js/fiveui/injected/ui.js b/src/js/fiveui/injected/ui.js
index 8bedc46..03a1899 100644
--- a/src/js/fiveui/injected/ui.js
+++ b/src/js/fiveui/injected/ui.js
@@ -181,8 +181,6 @@
 
        if(height != this.height) {
 
-         console.log('changing height');
-
          this.height = height;
 
          var ppos = this.$problems.position();
-- 
cgit v1.2.3