etc/options
changeset 48457 fd9e28d5a143
parent 48370 d0fa3efec93b
child 48458 09710d6fc3d1
     1.1 --- a/etc/options	Mon Jul 23 22:35:10 2012 +0200
     1.2 +++ b/etc/options	Tue Jul 24 00:29:36 2012 +0200
     1.3 @@ -6,6 +6,7 @@
     1.4  declare document_format : string = pdf
     1.5  declare document_variants : string = document
     1.6  declare document_graph : bool = false
     1.7 +declare document_dump : string = ""
     1.8  
     1.9  declare threads_limit : int = 1
    1.10  declare threads_trace : int = 0
    1.11 @@ -18,7 +19,6 @@
    1.12  declare quick_and_dirty : bool = false
    1.13  
    1.14  declare timing : bool = false
    1.15 -declare verbose : bool = false
    1.16  
    1.17  declare condition : string = ""
    1.18