# HG changeset patch
# User wenzelm
# Date 1343125201 -7200
# Node ID 7f2998b9524972f11e07ee6dba630de6cae48a1d
# Parent  a4318c36a829fdc5cea5dd6327c78a3333934de3
added "document_dump_only" (cf. negated usedir -C);

diff -r a4318c36a829 -r 7f2998b95249 etc/options
--- a/etc/options	Tue Jul 24 12:14:16 2012 +0200
+++ b/etc/options	Tue Jul 24 12:20:01 2012 +0200
@@ -7,6 +7,7 @@
 declare document_variants : string = "outline=/proof,/ML"
 declare document_graph : bool = false
 declare document_dump : string = ""
+declare document_dump_only : bool = false
 declare no_document : bool = false
 
 declare threads : int = 0
diff -r a4318c36a829 -r 7f2998b95249 src/Pure/System/build.ML
--- a/src/Pure/System/build.ML	Tue Jul 24 12:14:16 2012 +0200
+++ b/src/Pure/System/build.ML	Tue Jul 24 12:20:01 2012 +0200
@@ -55,14 +55,11 @@
         (Options.bool options "document_graph")
         (space_explode ":" (Options.string options "document_variants"))
         parent base_name
-        (true (* FIXME copy document/ files on Scala side!? *),
-          Options.string options "document_dump")
+        (not (Options.bool options "document_dump_only"), Options.string options "document_dump")
         (Options.string options "browser_info_remote")
         verbose;
-
     val _ = Session.with_timing name timing (List.app use_theories) theories;
     val _ = Session.finish ();
-
     val _ = if save then () else quit ();
   in () end
   handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);