shortname: $strhelp", "$course->fullname",
"id\">$course->shortname -> $strhelp");
} else {
if (! $site = get_site()) {
error("Site is misconfigured");
}
$strdocumentation = get_string("documentation");
print_header("$site->shortname: $strhelp", "$site->fullname",
"$strdocumentation");
}
echo "";
document_file($file, true);
echo "
";
?>