diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2011-01-06 14:25:42 -0500 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2011-01-06 14:25:42 -0500 |
| commit | ef58d6735426a9ab3e6a7643c65926e362f7d157 (patch) | |
| tree | fa620106b21cda5516c17d6ab697326b9066c5fd /lib/js | |
| parent | e2ce533559f5669a13d663c74d65610079162448 (diff) | |
Client-side redirects
Diffstat (limited to 'lib/js')
| -rw-r--r-- | lib/js/urweb.js | 4 |
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); |