src/Pure/System/build.ML
changeset 49477 424fd5364f15
parent 49476 96c1ef26aabe
child 49478 07f752935ece
     1.1 --- a/src/Pure/System/build.ML	Tue Jul 24 10:44:36 2012 +0200
     1.2 +++ b/src/Pure/System/build.ML	Tue Jul 24 10:58:43 2012 +0200
     1.3 @@ -35,15 +35,12 @@
     1.4          end;
     1.5  
     1.6      val _ =
     1.7 -      Session.init
     1.8 -        save
     1.9 -        false (* FIXME reset!? *)
    1.10 +      Session.init save false
    1.11          (Options.bool options "browser_info") browser_info
    1.12          (Options.string options "document")
    1.13          (Options.bool options "document_graph")
    1.14          (space_explode "," (Options.string options "document_variants"))
    1.15 -        parent
    1.16 -        base_name
    1.17 +        parent base_name
    1.18          (true (* FIXME copy document/ files on Scala side!? *),
    1.19            Options.string options "document_dump")
    1.20          ""