$file"; echo '

';
		echo htmlspecialchars(file_get_contents($file));
		echo '

'; } }