A script that will jump to a given URL. Very simple.

diff --git a/course/jumpto.php b/course/jumpto.php
new file mode 100644 (file)
index 0000000..93a40fb
--- /dev/null
+++ b/course/jumpto.php
@@ -0,0 +1,18 @@
+<?php  // $Id$
+       
+/*
+ * Jumps to a given URL.  Mostly used for accessibility.
+ *
+ */
+
+require('../config.php');
+
+$jump = parameter('jump');
+
+if ($jump) {
+    redirect(urldecode($jump));
+}
+
+redirect($_SERVER['HTTP_REFERER']);
+
+?>