etc/options
changeset 48468 7f2998b95249
parent 48466 3b2fb20df17d
child 48486 691d0b44a793
--- a/etc/options	Tue Jul 24 12:14:16 2012 +0200
+++ b/etc/options	Tue Jul 24 12:20:01 2012 +0200
@@ -7,6 +7,7 @@
 declare document_variants : string = "outline=/proof,/ML"
 declare document_graph : bool = false
 declare document_dump : string = ""
+declare document_dump_only : bool = false
 declare no_document : bool = false
 
 declare threads : int = 0