915
951
/* This used to be an fputs(), but since the string might contain NUL's,
918
#define ECHO fwrite( yytext, yyleng, 1, yyout )
954
#define ECHO do { if (fwrite( yytext, yyleng, 1, yyout )) {} } while (0)
921
957
/* Gets input and stuffs it into "buf". number of characters read, or YY_NULL,