1.1 --- a/src/Pure/System/build.ML Tue Jul 24 11:14:37 2012 +0200
1.2 +++ b/src/Pure/System/build.ML Tue Jul 24 11:39:22 2012 +0200
1.3 @@ -53,7 +53,7 @@
1.4 (Options.bool options "browser_info") browser_info
1.5 (Options.string options "document")
1.6 (Options.bool options "document_graph")
1.7 - (space_explode "," (Options.string options "document_variants"))
1.8 + (space_explode ":" (Options.string options "document_variants"))
1.9 parent base_name
1.10 (true (* FIXME copy document/ files on Scala side!? *),
1.11 Options.string options "document_dump")