diff -r 3e17f343deb5 -r c5d0f19ef7cb etc/options
--- 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