From ef58d6735426a9ab3e6a7643c65926e362f7d157 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Thu, 6 Jan 2011 14:25:42 -0500
Subject: Client-side redirects

---
 lib/js/urweb.js | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'lib/js/urweb.js')

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);
-- 
cgit v1.2.3