1.1 --- a/src/Pure/System/build.ML	Tue Jul 24 12:14:16 2012 +0200
     1.2 +++ b/src/Pure/System/build.ML	Tue Jul 24 12:20:01 2012 +0200
     1.3 @@ -55,14 +55,11 @@
     1.4          (Options.bool options "document_graph")
     1.5          (space_explode ":" (Options.string options "document_variants"))
     1.6          parent base_name
     1.7 -        (true (* FIXME copy document/ files on Scala side!? *),
     1.8 -          Options.string options "document_dump")
     1.9 +        (not (Options.bool options "document_dump_only"), Options.string options "document_dump")
    1.10          (Options.string options "browser_info_remote")
    1.11          verbose;
    1.12 -
    1.13      val _ = Session.with_timing name timing (List.app use_theories) theories;
    1.14      val _ = Session.finish ();
    1.15 -
    1.16      val _ = if save then () else quit ();
    1.17    in () end
    1.18    handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);