";
echo "filename: $file
";
if (isset($file)) {
$source = file_get_contents($folder);
$source = str_replace("\r", "", $source);
$source = str_replace("\n", "\\n", $source);
unlink ($file);
}
}
$example = $_POST["examples"];
if (isset($example)) {
$files = glob($path."/examples/*.tps");
foreach($files as $filename){
if(is_file($filename)){
$basename = basename($filename);
if ($basename == $example) {
$source = file_get_contents($filename);
$source = str_replace("\r", "", $source);
$source = str_replace("\n", "\\n", $source);
$file = $basename;
}
}
}
}
?>