double header in error() workaround

diff --git a/lib/weblib.php b/lib/weblib.php
index a86b59902d3a538918875a101d6fa6e29c3255f4..7bd5d8adda6844a8a5e6c45374c51492a8eb7826 100644 (file)
--- a/lib/weblib.php
+++ b/lib/weblib.php
@@ -4029,9 +4029,12 @@ function print_scale_menu_helpbutton($courseid, $scale) {
 function error ($message, $link='') {
     global $CFG, $SESSION;
 
-    @header('HTTP/1.0 404 Not Found');
+    if (!headers_sent()) {
+        //header not yet printed
+        @header('HTTP/1.0 404 Not Found');
+        print_header(get_string('error'));
+    }
 
-    print_header(get_string('error'));
     echo '<br />';
 
     $message = clean_text($message);   // In case nasties are in here