diff --git a/lib/weblib.php b/lib/weblib.php
index 58e772b997e..8e5e26a69ab 100644
--- a/lib/weblib.php
+++ b/lib/weblib.php
@@ -4801,7 +4801,7 @@ function redirect($url, $message='', $delay=-1) {
@header('Location: '.$url);
//another way for older browsers and already sent headers (eg trailing whitespace in config.php)
echo '';
- echo ''; // To cope with Mozilla bug
+ echo ''; // To cope with Mozilla bug
die;
}