etc/options
changeset 48516 c5d0f19ef7cb
parent 48513 ace120a2cb70
child 48520 6d4ea2efa64b
--- a/etc/options	Thu Jul 26 14:24:27 2012 +0200
+++ b/etc/options	Thu Jul 26 14:29:54 2012 +0200
@@ -6,7 +6,7 @@
 declare document_variants : string = "outline=/proof,/ML"
 declare document_graph : bool = false
 declare document_dump : string = ""
-declare document_dump_only : bool = false
+declare document_dump_mode : string = "all"
 declare no_document : bool = false
 
 declare threads : int = 0