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

diff --git a/src/cfgparse.y b/src/cfgparse.y
index 1669b4ab7b854f992733e325a50c23305082af5c..a33ecaf11f5c73ed996784a3841fe7318701fa46 100644 (file)
--- a/src/cfgparse.y
+++ b/src/cfgparse.y
@@ -404,7 +404,7 @@ workspace:
 
 optional_workspace_name:
         /* empty */                     { $<string>$ = NULL; }
-        | workspace_name                { $<string>$ = $<string>1; }
+        | WHITESPACE workspace_name     { $<string>$ = $<string>1; }
         ;
 
 workspace_name: