1.1 --- a/src/Pure/System/build.ML	Thu Jul 26 12:32:25 2012 +0200
     1.2 +++ b/src/Pure/System/build.ML	Thu Jul 26 12:59:09 2012 +0200
     1.3 @@ -50,7 +50,7 @@
     1.4  
     1.5  fun build args_file =
     1.6    let
     1.7 -    val (save, (options, (timing, (verbose, (browser_info, (parent_base_name,
     1.8 +    val (do_output, (options, (timing, (verbose, (browser_info, (parent_base_name,
     1.9          (name, (base_name, theories)))))))) =
    1.10        File.read (Path.explode args_file) |> YXML.parse_body |>
    1.11          let open XML.Decode in
    1.12 @@ -59,7 +59,7 @@
    1.13          end;
    1.14  
    1.15      val _ =
    1.16 -      Session.init save false
    1.17 +      Session.init do_output false
    1.18          (Options.bool options "browser_info") browser_info
    1.19          (Options.string options "document")
    1.20          (Options.bool options "document_graph")
    1.21 @@ -70,7 +70,7 @@
    1.22          verbose;
    1.23      val _ = Session.with_timing name timing (List.app use_theories) theories;
    1.24      val _ = Session.finish ();
    1.25 -    val _ = if save then () else quit ();
    1.26 +    val _ = if do_output then () else quit ();
    1.27    in () end
    1.28    handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
    1.29