1 files changed, 9 insertions, 1 deletions
diff --git a/lib/js/urweb.js b/lib/js/urweb.js
index 2943c897..d0322bff 100644
--- a/lib/js/urweb.js
+++ b/lib/js/urweb.js
@@ -301,11 +301,19 @@ function inp(t, s, content) {
   return x;
 }
 
+function addOnChange(x, f) {
+  var old = x.onchange;
+  x.onchange = function() { old(); f (); };
+}
+
 
 // Basic string operations
 
 function eh(x) {
-  return x.split("&").join("&amp;").split("<").join("&lt;").split(">").join("&gt;");
+  if (x == null)
+    return "NULL";
+  else
+    return x.split("&").join("&amp;").split("<").join("&lt;").split(">").join("&gt;");
 }
 
 function ts(x) { return x.toString() }