changeset 48457 | fd9e28d5a143 |
parent 48370 | d0fa3efec93b |
child 48458 | 09710d6fc3d1 |
--- a/etc/options Mon Jul 23 22:35:10 2012 +0200 +++ b/etc/options Tue Jul 24 00:29:36 2012 +0200 @@ -6,6 +6,7 @@ declare document_format : string = pdf declare document_variants : string = document declare document_graph : bool = false +declare document_dump : string = "" declare threads_limit : int = 1 declare threads_trace : int = 0 @@ -18,7 +19,6 @@ declare quick_and_dirty : bool = false declare timing : bool = false -declare verbose : bool = false declare condition : string = ""