1 files changed, 8 insertions, 0 deletions
diff --git a/lib/js/urweb.js b/lib/js/urweb.js
index 45ed6be8..6cf8a3f3 100644
--- a/lib/js/urweb.js
+++ b/lib/js/urweb.js
@@ -1475,6 +1475,14 @@ function strcmp(str1, str2) {
     return ((str1 == str2) ? 0 : ((str1 > str2) ? 1 : -1));
 }
 
+function chr(n) {
+    return String.fromCharCode(n);
+}
+
+function htmlifySpecialChar(ch) {
+    return "&#" + ch.charCodeAt(0) + ";";
+}
+
 
 // Remote calls