etc/options
changeset 50121 97d2b77313a0
parent 50119 5c370a036de7
child 50255 d0ec1f0d1d7d
--- a/etc/options	Sun Nov 18 16:31:41 2012 +0100
+++ b/etc/options	Sun Nov 18 19:01:30 2012 +0100
@@ -13,10 +13,6 @@
   -- "option alternative document variants (separated by colons)"
 option document_graph : bool = false
   -- "generate session graph image for document"
-option document_dump : string = ""
-  -- "dump generated document sources into given directory"
-option document_dump_mode : string = "all"
-  -- "specific document dump mode: all, tex, tex+sty"
 
 option show_question_marks : bool = true
   -- "show leading question mark of schematic variables"