Fixed Mozilla redirection-after-htmlediting bug using Javascript!

diff --git a/lib/weblib.php b/lib/weblib.php
index 02d9cc9b7eb6ff425f2c7aca7067e33f42e24c58..457d0f42cd878089aacb52c814d503ce640e88d5 100644 (file)
--- a/lib/weblib.php
+++ b/lib/weblib.php
@@ -1679,6 +1679,9 @@ function redirect($url, $message="", $delay="0") {
         echo "<p>$message</p>";
         echo "<p>( <a href=\"$url\">".get_string("continue")."</a> )</p>";
         echo "</center>";
+        flush();
+        sleep($delay);
+        echo "<script>location.replace('$url');</script>";   // To cope with Mozilla bug
     }
     die; 
 }