src/Pure/System/build.ML
changeset 49497 45137257399a
parent 49492 322fbf571782
child 49501 691d0b44a793
     1.1 --- a/src/Pure/System/build.ML	Tue Jul 24 18:38:07 2012 +0200
     1.2 +++ b/src/Pure/System/build.ML	Tue Jul 24 20:41:50 2012 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4  
     1.5  fun build args_file =
     1.6    let
     1.7 -    val (save, (options, (timing, (verbose, (browser_info, (parent,
     1.8 +    val (save, (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 @@ -55,7 +55,7 @@
    1.13          (Options.string options "document")
    1.14          (Options.bool options "document_graph")
    1.15          (space_explode ":" (Options.string options "document_variants"))
    1.16 -        parent base_name
    1.17 +        parent_base_name base_name
    1.18          (not (Options.bool options "document_dump_only"), Options.string options "document_dump")
    1.19          (Options.string options "browser_info_remote")
    1.20          verbose;