Fix for bug #5571 (by mookid@sigent.ru)

diff --git a/Zend/zend_ini_scanner.l b/Zend/zend_ini_scanner.l
index dcb0998f68ba7c09431f7311fc894816893196b6..af407b237299dd3f177d00fee35e6b133fdd1b5d 100644 (file)
--- a/Zend/zend_ini_scanner.l
+++ b/Zend/zend_ini_scanner.l
@@ -276,3 +276,8 @@ void zend_ini_close_file(zend_file_handle *fh)
        php_error(E_NOTICE,"Unexpected character on line %d:  '%s' (ASCII %d)\n",yylineno,yytext,yytext[0]);
 #endif
 }
+
+<<EOF>> {
+       yy_delete_buffer(YY_CURRENT_BUFFER);
+       yyterminate();
+}