diff --git a/lib/weblib.php b/lib/weblib.php index e04433498c8..e9b1df4ab7d 100644 --- a/lib/weblib.php +++ b/lib/weblib.php @@ -2403,8 +2403,8 @@ function print_navigation ($navigation) { if (! $site = get_site()) { $site->shortname = get_string('home'); } - $navigation = '