dep-ui.js: Add the CAPTUREP argument to `addEventListener' calls.

Otherwise MicroB, at least, throws exceptions.

diff --git a/dep-ui.js b/dep-ui.js
index 22f2e60..54f97b5 100644 (file)
--- a/dep-ui.js
+++ b/dep-ui.js
@@ -139,9 +139,9 @@ DEP_UI.input_field = function (id, dep, convert) {
   // Arrange to update the dep `shortly after' updates.
   var soon = new Soon(kick);
   function kick_soon () { soon.kick(); }
-  e.addEventListener('click', kick_soon);
-  e.addEventListener('blur', kick_soon);
-  e.addEventListener('keypress', kick_soon);
+  e.addEventListener('click', kick_soon, false);
+  e.addEventListener('blur', kick_soon, false);
+  e.addEventListener('keypress', kick_soon, false);
 
   // Sadly, the collection of events above isn't comprehensive, because we
   // don't actually get told about edits as a result of clipboard operations,
@@ -169,8 +169,8 @@ DEP_UI.input_radio = function (id, dep) {
   // Arrange to update the dep `shortly after' updates.
   var soon = new Soon(kick);
   function kick_soon () { soon.kick(); }
-  e.addEventListener('click', kick_soon);
-  e.addEventListener('changed', kick_soon);
+  e.addEventListener('click', kick_soon, false);
+  e.addEventListener('changed', kick_soon, false);
 
   // The situation for radio buttons doesn't seem as bad as for text widgets,
   // but let's be on the safe side.
@@ -216,7 +216,7 @@ function kick_all() {
 setInterval(kick_all, 500);
 
 // And make sure we get everything started when the page is fully loaded.
-window.addEventListener('load', kick_all);
+window.addEventListener('load', kick_all, false);
 
 /*----- That's all, folks -------------------------------------------------*/
 } })();