diff -r d8ff14f44a40 -r fd9e28d5a143 etc/options
--- 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 = ""