summaryrefslogtreecommitdiff
path: root/lib/js
diff options
context:
space:
mode:
Diffstat (limited to 'lib/js')
-rw-r--r--lib/js/urweb.js4
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);