Bugfix: WHITESPACE was missing in front of the workspace name (Thanks Mirko)

This commit is contained in:
Michael Stapelberg 2009-11-08 21:43:47 +01:00
parent 316f62dfda
commit f2dcc36333
1 changed files with 1 additions and 1 deletions

View File

@ -404,7 +404,7 @@ workspace:
optional_workspace_name: optional_workspace_name:
/* empty */ { $<string>$ = NULL; } /* empty */ { $<string>$ = NULL; }
| workspace_name { $<string>$ = $<string>1; } | WHITESPACE workspace_name { $<string>$ = $<string>1; }
; ;
workspace_name: workspace_name: