function copy_text_file($source, $dest)
{
$text = file_get_contents($source);
- $text = preg_replace("/[^\r]\n$/", "\r\n", $text);
+ $text = preg_replace("/(\r\n?)|\n/", "\r\n", $text);
$fp = fopen($dest, "w");
fwrite($fp, $text);
fclose($fp);
"NEWS" => "news.txt",
"php.ini-dist" => "php.ini-dist",
"php.ini-recommended" => "php.ini-recommended",
+ "win32/install.txt" => "install.txt",
);
foreach ($text_files as $src => $dest) {
/* general other files */
$general_files = array(
- "win32/install.txt" => "install.txt",
"php.gif" => "php.gif",
);