etc/options
changeset 48458 09710d6fc3d1
parent 48457 fd9e28d5a143
child 48459 375e45df6fdf
     1.1 --- a/etc/options	Tue Jul 24 00:29:36 2012 +0200
     1.2 +++ b/etc/options	Tue Jul 24 10:11:49 2012 +0200
     1.3 @@ -2,11 +2,11 @@
     1.4  
     1.5  declare browser_info : bool = false
     1.6  
     1.7 -declare document : bool = true
     1.8 -declare document_format : string = pdf
     1.9 +declare document : string = ""
    1.10  declare document_variants : string = document
    1.11  declare document_graph : bool = false
    1.12  declare document_dump : string = ""
    1.13 +declare no_document : bool = false
    1.14  
    1.15  declare threads_limit : int = 1
    1.16  declare threads_trace : int = 0