src/Pure/System/build.ML
changeset 48516 c5d0f19ef7cb
parent 48513 ace120a2cb70
child 48520 6d4ea2efa64b
     1.1 --- a/src/Pure/System/build.ML	Thu Jul 26 14:24:27 2012 +0200
     1.2 +++ b/src/Pure/System/build.ML	Thu Jul 26 14:29:54 2012 +0200
     1.3 @@ -65,7 +65,7 @@
     1.4          (Options.bool options "document_graph")
     1.5          (space_explode ":" (Options.string options "document_variants"))
     1.6          parent_base_name base_name
     1.7 -        (not (Options.bool options "document_dump_only"), Options.string options "document_dump")
     1.8 +        (Options.string options "document_dump", Options.string options "document_dump_mode")
     1.9          "" verbose;
    1.10      val _ = Session.with_timing name timing (List.app use_theories) theories;
    1.11      val _ = Session.finish ();