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