From ff0194552229473b9a77e15a634b522359172ee6 Mon Sep 17 00:00:00 2001
From: moodler <moodler>
Date: Sat, 1 Nov 2003 06:59:31 +0000
Subject: [PATCH] Fixed Mozilla redirection-after-htmlediting bug using
 Javascript!

---
 lib/weblib.php | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/lib/weblib.php b/lib/weblib.php
index 02d9cc9b7e..457d0f42cd 100644
--- 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; 
 }
-- 
2.39.5