$msg_text EOF; exit; } /* возвращает строку содержащую имя файла и номер строки в нем */ function make_line($file, $line) { return "$file:$line"; } ?>