--- a/src/Pure/System/build.ML Fri Jul 27 12:43:58 2012 +0200
+++ b/src/Pure/System/build.ML Fri Jul 27 13:01:19 2012 +0200
@@ -71,7 +71,8 @@
(Options.bool options "document_graph")
(space_explode ":" (Options.string options "document_variants"))
parent_name name
- (Options.string options "document_dump", Options.string options "document_dump_mode")
+ (Options.string options "document_dump",
+ Present.dump_mode (Options.string options "document_dump_mode"))
"" verbose;
val _ = Session.with_timing name timing (List.app use_theories) theories;
val _ = Session.finish ();