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