+
+<*>^#[ \t]*line[ \t]+[0-9]+([ \t]\"[^\n\r\f\"]*\")? {
+ char *p;
+ char *number;
+ char *filename;
+ char *str=g_strdup(yytext);
+
+ /* find first digit of line number */
+ p=str;
+ while(*p&&!isdigit(*p)) p++;
+ number=p;
+
+ /* find end of line number */
+ while(*p&&isdigit(*p)) p++;
+ if(*p) *p++=0;
+
+ /* find beginning of filename */
+ p=strchr(p,'"');
+ if(p) p++;
+ filename=p;
+
+ /* find end of filename */
+ if(p) p=strchr(p,'"');
+ if(p) *p=0;
+
+ /* stash number (minus one because we don't count this line) */
+ if(number) line_no=atoi(number)-1;
+
+ /* stash filename */
+ if(filename) {
+ if(hline_filename) g_free(hline_filename);
+ hline_filename=g_strdup(filename);
+ }
+
+ /* clean up */
+ g_free(str);
+}
+