--- a/src/Pure/System/build.ML Tue Aug 14 13:40:49 2012 +0200
+++ b/src/Pure/System/build.ML Tue Aug 14 15:42:58 2012 +0200
@@ -68,10 +68,15 @@
val document_variants =
map Present.read_variant (space_explode ":" (Options.string options "document_variants"));
val _ =
+ (case duplicates (op =) (map fst document_variants) of
+ [] => ()
+ | dups => error ("Duplicate document variants: " ^ commas_quote dups));
+ val _ =
Session.init do_output false
(Options.bool options "browser_info") browser_info
(Options.string options "document")
(Options.bool options "document_graph")
+ (Options.string options "document_output")
document_variants
parent_name name
(Options.string options "document_dump",