", "\n", $code);
$code = str_replace(" ", " ", $code);
return $matches[1] . $code . $matches[3];
}
$path = dirname(dirname(__FILE__));
$iter = new DirectoryIterator("$path/output/manual");
foreach ($iter as $file) {
if ($file->isFile()) {
$name = $file->getPathName();
$html = file_get_contents($name);
$html = preg_replace_callback('/()(.*?)(<\/pre>)/s', "highlight", $html);
file_put_contents($name, $html);
}
}