src/Pure/System/build.ML
changeset 49481 3b2fb20df17d
parent 49480 a25daffda966
child 49483 7f2998b95249
     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")