call onFinish in reproduceriter

1 files changed, 10 insertions, 0 deletions

diff --git a/tools/reproduceriter.py b/tools/reproduceriter.py
index 3638b882..3402192c 100755
--- a/tools/reproduceriter.py
+++ b/tools/reproduceriter.py
@@ -265,6 +265,7 @@ var Recorder = (function() {
       if (recorder.randoms.length > 0) {
         return recorder.randoms.pop();
       } else {
+        recorder.finish();
         throw 'consuming too many values!';
       }
     };
@@ -273,6 +274,7 @@ var Recorder = (function() {
       if (recorder.dnows.length > 0) {
         return recorder.dnows.pop();
       } else {
+        recorder.finish();
         throw 'consuming too many values!';
       }
     };
@@ -280,6 +282,7 @@ var Recorder = (function() {
       if (recorder.pnows.length > 0) {
         return recorder.pnows.pop();
       } else {
+        recorder.finish();
         throw 'consuming too many values!';
       }
     };
@@ -291,6 +294,13 @@ var Recorder = (function() {
     recorder.addListener = function(target, which, callback, arg) {
       recorder['event' + which] = callback;
     };
+    // Finish
+    recorder.finish = function() {
+      if (recorder.onFinish) {
+        recorder.onFinish();
+        recorder.onFinish = null;
+      }
+    };
   }
   return recorder;
 })();