diff options
author | Adam Chlipala <adamc@hcoop.net> | 2009-01-08 10:30:14 -0500 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2009-01-08 10:30:14 -0500 |
commit | 9608c763d7b2923c11e8abd29e28271ae470a5fe (patch) | |
tree | d4648aecea89bd3799de7a6ee50a6333bd967e1a /jslib/urweb.js | |
parent | 4b109c964ac7f433b4feb9d28b135dee28f75b87 (diff) |
Injected a non-special-case datatype
Diffstat (limited to 'jslib/urweb.js')
-rw-r--r-- | jslib/urweb.js | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/jslib/urweb.js b/jslib/urweb.js index 16424eb3..9d28b461 100644 --- a/jslib/urweb.js +++ b/jslib/urweb.js @@ -41,6 +41,10 @@ function dyn(s) { s.h = cons(function() { x.innerHTML = s.v }, s.h); } +function eh(x) { + return x.split("&").join("&").split("<").join("<").split(">").join(">"); +} + function ts(x) { return x.toString() } function bs(b) { return (b ? "True" : "False") } |