diff -r 3e17f343deb5 -r c5d0f19ef7cb src/Pure/System/build.ML --- a/src/Pure/System/build.ML Thu Jul 26 14:24:27 2012 +0200 +++ b/src/Pure/System/build.ML Thu Jul 26 14:29:54 2012 +0200 @@ -65,7 +65,7 @@ (Options.bool options "document_graph") (space_explode ":" (Options.string options "document_variants")) parent_base_name base_name - (not (Options.bool options "document_dump_only"), Options.string options "document_dump") + (Options.string options "document_dump", Options.string options "document_dump_mode") "" verbose; val _ = Session.with_timing name timing (List.app use_theories) theories; val _ = Session.finish ();