diff lib/js/urweb.js @ 1385:449a12b82db7

Client-side redirects
author Adam Chlipala <adam@chlipala.net>
date Thu, 06 Jan 2011 14:25:42 -0500
parents 02fc16faecf3
children 36f7d1debb37
line wrap: on
line diff
--- a/lib/js/urweb.js	Thu Jan 06 12:49:14 2011 -0500
+++ b/lib/js/urweb.js	Thu Jan 06 14:25:42 2011 -0500
@@ -715,6 +715,10 @@
     return parse(s);
 }
 
+function redirect(s) {
+    window.location = s;
+}
+
 function rc(prefix, uri, parse, k, needsSig) {
     uri = cat(prefix, uri);
     uri = flattenLocal(uri);