1 files changed, 4 insertions, 0 deletions
diff --git a/lib/js/urweb.js b/lib/js/urweb.js
index bba58453..3cb667d6 100644
--- a/lib/js/urweb.js
+++ b/lib/js/urweb.js
@@ -715,6 +715,10 @@ function unurlify(parse, s) {
     return parse(s);
 }
 
+function redirect(s) {
+    window.location = s;
+}
+
 function rc(prefix, uri, parse, k, needsSig) {
     uri = cat(prefix, uri);
     uri = flattenLocal(uri);