From 8316c65b174e881433721382e0214cec2412ae6b Mon Sep 17 00:00:00 2001
From: Trevor Elliott <trevor@galois.com>
Date: Mon, 17 Jun 2013 17:17:09 -0700
Subject: Fix a funny bug that caused a closed port to be used

---
 src/js/fiveui/injected/compute.js | 10 ----------
 1 file changed, 10 deletions(-)

(limited to 'src/js/fiveui/injected/compute.js')

diff --git a/src/js/fiveui/injected/compute.js b/src/js/fiveui/injected/compute.js
index 8fc7a84..7ba4af4 100644
--- a/src/js/fiveui/injected/compute.js
+++ b/src/js/fiveui/injected/compute.js
@@ -90,15 +90,6 @@
      core.port.emit('ReportProblem', prob);
    };
 
-   core.resetStats = function() {
-     core.reportStats(
-       { start:    0
-       , end:      0
-       , numRules: 0
-       , numElts:  0
-       });
-   };
-
    core.reportStats = function(stats) {
      core.port.emit('ReportStats', stats);
    };
@@ -356,6 +347,5 @@
    };
 
    registerBackendListeners(core.port);
-   core.resetStats();
 })();
 
-- 
cgit v1.2.3